awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
grw :
  (↑(1 * I) : Submodule R A) ≤
    HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
grw₁ :
  (↑1 : Submodule R A) * (↑I : Submodule R A) ≤
    HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
grw₂ :
  1 * (↑I : Submodule R A) ≤
    HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
⊢ (↑(1 * I) : Submodule R A) ≤ span R (↑T : Set A) * (↑I⁻¹ : Submodule R A) * (↑I : Submodule R A)
have grw₃ : 1 * (↑I : Submodule R A) ≤ span R ((↑T : Set A) * (↑T' : Set A)) * (↑I : Submodule R A)
Tactic: grw [← span_le.mpr hT', Units.val_mul, Units.val_one, span_mul_span, one_le.2 one_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
one_mem : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) 1
grw :
  (↑(1 * I) : Submodule R A) ≤
    HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
grw₁ :
  (↑1 : Submodule R A) * (↑I : Submodule R A) ≤
    HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
grw₂ :
  1 * (↑I : Submodule R A) ≤
    HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) (span R (↑T' : Set A)) * (↑I : Submodule R A)
grw₃ : 1 * (↑I : Submodule R A) ≤ span R ((↑T : Set A) * (↑T' : Set A)) * (↑I : Submodule R A)
⊢ (↑(1 * I) : Submodule R A) ≤ span R (↑T : Set A) * (↑I⁻¹ : Submodule R A) * (↑I : Submodule R A)
have grw₄ : span R ((↑T : Set A) * (↑T' : Set A)) * (↑I : Submodule R A) ≤
  span R ((↑T : Set A) * (↑T' : Set A)) * (↑I : Submodule R A)
Tactic: grw [← span_le.mpr hT', Units.val_mul, Units.val_one, span_mul_span, one_le.2 one_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
hm : M.FG
hn : N.FG
⊢ (M * N).FG
have rw : (Submodule.map₂ (LinearMap.mul R A) M N).FG
Tactic: rw [mul_eq_map₂]
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h : Fintype.card R ≤ 2
⊢ Eq (α := Finset R) univ {0, 1}
have inl : Subsingleton R → Eq (α := Finset R) univ {0, 1}
Tactic: rcases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h : Fintype.card R ≤ 2
inl : Subsingleton R → Eq (α := Finset R) univ {0, 1}
⊢ Eq (α := Finset R) univ {0, 1}
have inr : Nontrivial R → Eq (α := Finset R) univ {0, 1}
Tactic: rcases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h : Fintype.card R ≤ 2
h_1 : Nontrivial R
⊢ Eq (α := Finset R) univ {0, 1}
have inr : card.{u_1} (α := R) univ ≤ card (α := R) {0, 1}
Tactic: refine (eq_of_subset_of_card_le (subset_univ _) ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h : Fintype.card R ≤ 2
h_1 : Nontrivial R
⊢ card.{u_1} (α := R) univ ≤ card (α := R) {0, 1}
have h₁ : card (α := R) {0, 1} = 2
Tactic: convert! h
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h : Fintype.card R ≤ 3
⊢ Eq (α := Finset R) univ {0, 1, -1}
have refine : card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
Tactic: refine (eq_of_subset_of_card_le (subset_univ _) ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h : Fintype.card R ≤ 3
⊢ card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
have inl : ∀ (h : Fintype.card R < 3), card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
Tactic: rcases lt_or_eq_of_le h with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h : Fintype.card R ≤ 3
inl : ∀ (h : Fintype.card R < 3), card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
⊢ card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
have inr : ∀ (h : Fintype.card R = 3), card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
Tactic: rcases lt_or_eq_of_le h with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
have inl : Subset (α := Finset R) univ {0, 1, -1}
Tactic: apply card_le_card
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ Subset (α := Finset R) univ {0, 1, -1}
have inl : Subset (α := Finset R) {0, 1} {0, 1, -1}
Tactic: rw [Finset.univ_of_card_le_two (Nat.lt_succ_iff.1 h)]
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ Nontrivial R
have refine : 1 < Fintype.card R
Tactic: refine Fintype.one_lt_card_iff_nontrivial.1 ?_
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ 1 < Fintype.card R
have rw : LT.lt (α := ℕ) 1 3
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
have this : Nontrivial R
Tactic: have : Nontrivial R := by
      refine Fintype.one_lt_card_iff_nontrivial.1 ?_
      rw [h]
      simp
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
have inr : 1 ∉ {-1}
Tactic: rw [card_univ, h, card_insert_of_notMem, card_insert_of_notMem, card_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
inr : 1 ∉ {-1}
⊢ card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
have inr₁ : 0 ∉ {1, -1}
Tactic: rw [card_univ, h, card_insert_of_notMem, card_insert_of_notMem, card_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ 1 ∉ {-1}
have inr : ¬Eq.{u_1 + 1} (α := R) 1 (-1)
Tactic: rw [mem_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : Eq.{u_1 + 1} (α := R) 1 (-1)
⊢ False
have H₁ : Eq.{u_1 + 1} (α := R) 2 0
Tactic: rw [← add_eq_zero_iff_eq_neg, one_add_one_eq_two] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : Eq.{u_1 + 1} (α := R) 2 0
⊢ False
have H₁ : Eq (α := ZMod 3)
  (((RingEquiv.symm (ringEquivOfPrime R Nat.prime_three h) : R ≃+* ZMod 3) : (a : R) → ZMod 3) 2 : ZMod 3)
  (((RingEquiv.symm (ringEquivOfPrime R Nat.prime_three h) : R ≃+* ZMod 3) : (a : R) → ZMod 3) 0 : ZMod 3)
Tactic: apply_fun (ringEquivOfPrime R Nat.prime_three h).symm at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H :
  Eq (α := ZMod 3)
    (((RingEquiv.symm (ringEquivOfPrime R Nat.prime_three h) : R ≃+* ZMod 3) : (a : R) → ZMod 3) 2 : ZMod 3)
    (((RingEquiv.symm (ringEquivOfPrime R Nat.prime_three h) : R ≃+* ZMod 3) : (a : R) → ZMod 3) 0 : ZMod 3)
⊢ False
have H₁ : Eq (α := ZMod 3) 2 0
Tactic: simp only [map_ofNat, map_zero] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : Eq (α := ZMod 3) 2 0
⊢ False
have H₁ : Eq (α := ZMod 3) (↑2 : ZMod 3) 0
Tactic: replace H : ((2 : ℕ) : ZMod 3) = 0 := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h_1 : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : Eq (α := ZMod 3) (↑2 : ZMod 3) 0
⊢ False
have H₁ : Dvd.dvd (α := ℕ) 3 2
Tactic: rw [natCast_eq_zero_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
⊢ Nat.card.{u_1} M₀ˣ < Nat.card M₀
have have : ∀ (this : Fintype M₀), Nat.card.{u_1} M₀ˣ < Nat.card M₀
Tactic: have : Fintype M₀ := Fintype.ofFinite M₀
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
a : M₀
⊢ orderOf a < Nat.card M₀
have pos : ∀ (h : IsUnit a), orderOf a < Nat.card M₀
Tactic: by_cases h : IsUnit a
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
a : M₀
pos : ∀ (h : IsUnit a), orderOf a < Nat.card M₀
⊢ orderOf a < Nat.card M₀
have neg : ∀ (h : ¬IsUnit a), orderOf a < Nat.card M₀
Tactic: by_cases h : IsUnit a
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
a : M₀
h : IsUnit a
⊢ orderOf a < Nat.card M₀
have pos : orderOf h.unit < Nat.card M₀
Tactic: rw [← h.unit_spec, orderOf_units]
-- Lean 4 proof step from Mathlib.RingTheory.Fintype (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
a : M₀
h : ¬IsUnit a
⊢ orderOf a < Nat.card M₀
have neg : 0 < Nat.card M₀
Tactic: rw [orderOf_eq_zero_iff'.mpr fun n hn ha ↦ h <| IsUnit.of_pow_eq_one ha hn.ne']
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
x y : N ⊗[R] M
eq :
  Eq (α := P ⊗[R] M) ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
    ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
⊢ x = y
have have : ∀ (N' : Submodule R N) (Nfg : N'.FG) (sub : {x, y} ⊆ (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))), x = y
Tactic: have ⟨N', Nfg, sub⟩ := Submodule.exists_fg_le_subset_range_rTensor_subtype {x, y} (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
x y : N ⊗[R] M
eq :
  Eq (α := P ⊗[R] M) ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
    ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
N' : Submodule R N
Nfg : N'.FG
sub : {x, y} ⊆ (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
⊢ x = y
have obtain : ∀ (x : TensorProduct.{u, u_1, v} R (↥N') M)
  (eq :
    Eq (α := P ⊗[R] M)
      ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x) : P ⊗[R] M)
      ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M))
  (sub :
    insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M) {y} ⊆
      (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))),
  (rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x = y
Tactic: obtain ⟨x, rfl⟩ := sub (.inl rfl)
Cleared hypotheses: x, eq, sub
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
y : N ⊗[R] M
N' : Submodule R N
Nfg : N'.FG
x : TensorProduct.{u, u_1, v} R (↥N') M
eq :
  Eq (α := P ⊗[R] M)
    ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x) : P ⊗[R] M)
    ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
sub :
  insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M) {y} ⊆
    (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
⊢ (rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x = y
have obtain : ∀ (y : TensorProduct.{u, u_1, v} R (↥N') M)
  (eq :
    Eq (α := P ⊗[R] M)
      ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x) : P ⊗[R] M)
      ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y) : P ⊗[R] M))
  (sub :
    insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
        (singleton (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)) ⊆
      (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))),
  Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
    ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
Tactic: obtain ⟨y, rfl⟩ := sub (.inr rfl)
Cleared hypotheses: y, eq, sub
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
N' : Submodule R N
Nfg : N'.FG
x y : TensorProduct.{u, u_1, v} R (↥N') M
eq :
  Eq (α := P ⊗[R] M)
    ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x) : P ⊗[R] M)
    ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y) : P ⊗[R] M)
sub :
  insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
      (singleton (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)) ⊆
    (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
⊢ Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
    ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
have eq₁ : Eq (α := P ⊗[R] M)
  ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
      ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
    P ⊗[R] M)
  ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
      ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
    P ⊗[R] M)
Tactic: simp_rw [← rTensor_comp_apply, show f ∘ₗ N'.subtype = (N'.map f).subtype ∘ₗ f.submoduleMap N'
    from rfl, rTensor_comp_apply] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
N' : Submodule R N
Nfg : N'.FG
x y : TensorProduct.{u, u_1, v} R (↥N') M
sub :
  insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
      (singleton (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)) ⊆
    (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
eq :
  Eq (α := P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
      P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
      P ⊗[R] M)
⊢ Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
    ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
have have : ∀ (P' : Submodule R P) (Pfg : P'.FG) (le : Submodule.map f N' ≤ P')
  (eq :
    Eq (α := TensorProduct.{u, u_2, v} R (↥P') M)
      ((rTensor M (inclusion le) : (a : ↥(Submodule.map f N') ⊗[R] M) → ↥P' ⊗[R] M)
          ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
        TensorProduct.{u, u_2, v} R (↥P') M)
      ((rTensor M (inclusion le) : (a : ↥(Submodule.map f N') ⊗[R] M) → ↥P' ⊗[R] M)
          ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
        TensorProduct.{u, u_2, v} R (↥P') M)),
  Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
    ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
Tactic: have ⟨P', Pfg, le, eq⟩ := (Nfg.map _).exists_rTensor_fg_inclusion_eq eq
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
N' : Submodule R N
Nfg : N'.FG
x y : TensorProduct.{u, u_1, v} R (↥N') M
sub :
  insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
      (singleton (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)) ⊆
    (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
eq_1 :
  Eq (α := P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
      P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
      P ⊗[R] M)
P' : Submodule R P
Pfg : P'.FG
le : Submodule.map f N' ≤ P'
eq :
  Eq (α := TensorProduct.{u, u_2, v} R (↥P') M)
    ((rTensor M (inclusion le) : (a : ↥(Submodule.map f N') ⊗[R] M) → ↥P' ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
      TensorProduct.{u, u_2, v} R (↥P') M)
    ((rTensor M (inclusion le) : (a : ↥(Submodule.map f N') ⊗[R] M) → ↥P' ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
      TensorProduct.{u, u_2, v} R (↥P') M)
⊢ Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
    ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
have eq₁ : Eq (α := TensorProduct.{u, u_2, v} R (↥P') M)
  ((rTensor M (inclusion le ∘ₗ f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M) x :
    TensorProduct.{u, u_2, v} R (↥P') M)
  ((rTensor M (inclusion le ∘ₗ f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M) y :
    TensorProduct.{u, u_2, v} R (↥P') M)
Tactic: simp_rw [← rTensor_comp_apply] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
N' : Submodule R N
Nfg : N'.FG
x y : TensorProduct.{u, u_1, v} R (↥N') M
sub :
  insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
      (singleton (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)) ⊆
    (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
eq_1 :
  Eq (α := P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
      P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
      P ⊗[R] M)
P' : Submodule R P
Pfg : P'.FG
le : Submodule.map f N' ≤ P'
eq :
  Eq (α := TensorProduct.{u, u_2, v} R (↥P') M)
    ((rTensor M (inclusion le ∘ₗ f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M) x :
      TensorProduct.{u, u_2, v} R (↥P') M)
    ((rTensor M (inclusion le ∘ₗ f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M) y :
      TensorProduct.{u, u_2, v} R (↥P') M)
⊢ Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
    ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
have rw : Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
  ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
Tactic: rw [h _ _ Nfg Pfg (map_le_iff_le_comap.mp le) eq]