awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Small.{u, u_1} R
s : Finset S
⊢ Small.{u, u_2} ↥(adjoin R (↑s : Set S))

Tactic:
small_adjoin

Premises used: Algebra.small_adjoin
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Small.{u, u_1} R
s : Finset S
⊢ Small.{u, u_2} ↥(adjoin R (↑s : Set S))

Tactic:
exact small_adjoin

Premises used: Algebra.small_adjoin
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Small.{u, u_1} R
inst_4 : FiniteType R S
⊢ Small.{u, u_2} ↥⊤

Tactic:
have : Small.{u} (⊤ : Subalgebra R S) :=
    Subalgebra.FG.small Algebra.FiniteType.out
-- Module: Mathlib.RingTheory.Finiteness.Small
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Small.{u, u_1} R
inst_4 : FiniteType R S
this : Small.{u, u_2} ↥⊤
rwa rwa₁ rwa₂ rwa₃ : Small.{u, u_2} (↑Set.univ : Type u_2)
⊢ Small.{u, u_2} S

Tactic:
rwa [← small_univ_iff]

Premises used: small_univ_iff
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := Submodule R A) (span R (↑{1} : Set A)) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥)

Tactic:
simp [Algebra.toSubmodule_bot, one_eq_span]

Premises used: Algebra.toSubmodule_bot, Submodule.one_eq_span
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Module.Finite.{u_1, u_2} R ↥⊥

Tactic:
Module.Finite.range (Algebra.linearMap R A)

Premises used: Set.Mem, LinearMap.range, Algebra.linearMap, Module.Finite.range, Subsemiring.copy, AlgHom.range, Submodule.copy, RingHom.rangeS
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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)ˣ
obtain :
  ∀ (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), (↑I : Submodule R A).FG
⊢ (↑I : Submodule R A).FG

Tactic:
obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul (I.mul_inv ▸ one_le.mp le_rfl)

Premises used: Submodule.mem_span_mul_finite_of_mem_mul, OneMemClass.one_mem
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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
⊢ (↑I : Submodule R A).FG

Tactic:
⟨T, span_eq_of_le _ hT ?_⟩

Premises used: Submodule.span_eq_of_le, Submodule.FG, Exists.intro
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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
refine : (↑I : Submodule R A) ≤ span R (↑T : Set A)
⊢ (↑I : Submodule R A).FG

Tactic:
refine ⟨T, span_eq_of_le _ hT ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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
rw : (↑(1 * I) : Submodule R A) ≤ HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) 1
⊢ (↑I : Submodule R A) ≤ span R (↑T : Set A)

Tactic:
rw [← one_mul I, ← mul_one (span R (T : Set A))]

Premises used: SetLike.coe, Submodule.span, mul_one, one_mul
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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
rw : span R (↑T : Set A) * (↑I⁻¹ : Submodule R A) * (↑I : Submodule R A)
| HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) 1

Tactic:
rw [← I.inv_mul, ← mul_assoc]

Premises used: mul_assoc, Units.inv_mul
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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
conv_rhs : (↑(1 * I) : Submodule R A) ≤ span R (↑T : Set A) * (↑I⁻¹ : Submodule R A) * (↑I : Submodule R A)
⊢ (↑(1 * I) : Submodule R A) ≤ HMul.hMul (α := Submodule R A) (span R (↑T : Set A)) 1

Tactic:
conv_rhs => rw [← I.inv_mul, ← mul_assoc]

Premises used: mul_assoc, Units.inv_mul
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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)
grw₄ 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)
⊢ (↑(1 * I) : Submodule R A) ≤ span R (↑T : Set A) * (↑I⁻¹ : Submodule R 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]

Premises used: Iff.mpr, Submodule.span_mul_span, Units.val_one, Submodule.one_le, Submodule.span_le, Units.val_mul
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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
hI : IsUnit I
⊢ I.FG

Tactic:
fg_unit hI.unit

Premises used: IsUnit.unit, Submodule.fg_unit
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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
rw : (Submodule.map₂ (LinearMap.mul R A) M N).FG
⊢ (M * N).FG

Tactic:
rw [mul_eq_map₂]

Premises used: Submodule.mul_eq_map₂
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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
⊢ (Submodule.map₂ (LinearMap.mul R A) M N).FG

Tactic:
hm.map₂ _ hn

Premises used: Submodule.FG.map₂
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
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
⊢ (Submodule.map₂ (LinearMap.mul R A) M N).FG

Tactic:
exact hm.map₂ _ hn

Premises used: Submodule.FG.map₂
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submodule R A
h : M.FG
n : ℕ
⊢ span R (↑{1} : Set A) = M ^ Nat.zero

Tactic:
simp [one_eq_span]

Premises used: Submodule.one_eq_span
-- Module: Mathlib.RingTheory.Finiteness.Subalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submodule R A
h : M.FG
n_1 n : ℕ
ih : (M ^ n).FG
⊢ (M ^ n.succ).FG

Tactic:
simpa [pow_succ] using ih.mul h

Premises used: pow_succ, Submodule.FG.mul
-- Module: Mathlib.RingTheory.Fintype
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}
inr : Nontrivial R → Eq (α := Finset R) univ {0, 1}
⊢ Eq (α := Finset R) univ {0, 1}

Tactic:
rcases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Fintype
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h : Fintype.card R ≤ 2
h_1 : Subsingleton R
a : R
h_2 : Membership.mem (γ := Finset R) univ a
⊢ Membership.mem (γ := Finset R) {0, 1} a

Tactic:
simp [Subsingleton.elim a 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.Fintype
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h : Fintype.card R ≤ 2
h_1 : Subsingleton R
⊢ Eq (α := Finset R) univ {0, 1}

Tactic:
exact le_antisymm (fun a _ ↦ by simp [Subsingleton.elim a 0]) (Finset.subset_univ _)

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Fintype
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}

Tactic:
(eq_of_subset_of_card_le (subset_univ _) ?_).symm

Premises used: Finset.eq_of_subset_of_card_le, Eq.symm, Finset.subset_univ
-- Module: Mathlib.RingTheory.Fintype
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
inr : card.{u_1} (α := R) univ ≤ card (α := R) {0, 1}
⊢ Eq (α := Finset R) univ {0, 1}

Tactic:
refine (eq_of_subset_of_card_le (subset_univ _) ?_).symm

Premises used: Finset.eq_of_subset_of_card_le, Eq.symm, Finset.subset_univ
-- Module: Mathlib.RingTheory.Fintype
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
⊢ Fintype.card R ≤ 2

Tactic:
h
-- Module: Mathlib.RingTheory.Fintype
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
h₁ : card (α := R) {0, 1} = 2
⊢ card.{u_1} (α := R) univ ≤ card (α := R) {0, 1}

Tactic:
convert! h
-- Module: Mathlib.RingTheory.Fintype
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 (α := R) {0, 1} = 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Fintype
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}

Tactic:
(eq_of_subset_of_card_le (subset_univ _) ?_).symm

Premises used: Finset.eq_of_subset_of_card_le, Eq.symm, Finset.subset_univ
-- Module: Mathlib.RingTheory.Fintype
Goal:
R : Type u_1
inst : Ring R
inst_1 : Fintype R
inst_2 : DecidableEq R
h : Fintype.card R ≤ 3
refine : card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}
⊢ Eq (α := Finset R) univ {0, 1, -1}

Tactic:
refine (eq_of_subset_of_card_le (subset_univ _) ?_).symm

Premises used: Finset.eq_of_subset_of_card_le, Eq.symm, Finset.subset_univ
-- Module: Mathlib.RingTheory.Fintype
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}
inr : ∀ (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}

Tactic:
rcases lt_or_eq_of_le h with h | h

Premises used: lt_or_eq_of_le
-- Module: Mathlib.RingTheory.Fintype
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
inl : Subset (α := Finset R) univ {0, 1, -1}
⊢ card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}

Tactic:
apply card_le_card

Premises used: Finset.card_le_card
-- Module: Mathlib.RingTheory.Fintype
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
inl : Subset (α := Finset R) {0, 1} {0, 1, -1}
⊢ Subset (α := Finset R) univ {0, 1, -1}

Tactic:
rw [Finset.univ_of_card_le_two (Nat.lt_succ_iff.1 h)]

Premises used: Nat.lt_succ_iff, Iff.mp, Finset.univ_of_card_le_two
-- Module: Mathlib.RingTheory.Fintype
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) {0, 1} {0, 1, -1}

Tactic:
simp
-- Module: Mathlib.RingTheory.Fintype
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

Tactic:
Fintype.one_lt_card_iff_nontrivial.1 ?_

Premises used: Fintype.one_lt_card_iff_nontrivial, Iff.mp
-- Module: Mathlib.RingTheory.Fintype
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
refine : 1 < Fintype.card R
⊢ Nontrivial R

Tactic:
refine Fintype.one_lt_card_iff_nontrivial.1 ?_

Premises used: Fintype.one_lt_card_iff_nontrivial, Iff.mp
-- Module: Mathlib.RingTheory.Fintype
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
rw : LT.lt (α := ℕ) 1 3
⊢ 1 < Fintype.card R

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Fintype
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
⊢ LT.lt (α := ℕ) 1 3

Tactic:
simp
-- Module: Mathlib.RingTheory.Fintype
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

Tactic:
have : Nontrivial R := by
      refine Fintype.one_lt_card_iff_nontrivial.1 ?_
      rw [h]
      simp
-- Module: Mathlib.RingTheory.Fintype
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}
inr₁ : 0 ∉ {1, -1}
⊢ card.{u_1} (α := R) univ ≤ card (α := R) {0, 1, -1}

Tactic:
rw [card_univ, h, card_insert_of_notMem, card_insert_of_notMem, card_singleton]

Premises used: Finset.card_univ, Finset.card_insert_of_notMem, Finset.card_singleton
-- Module: Mathlib.RingTheory.Fintype
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 : ¬Eq.{u_1 + 1} (α := R) 1 (-1)
⊢ 1 ∉ {-1}

Tactic:
rw [mem_singleton]

Premises used: Finset.mem_singleton
-- Module: Mathlib.RingTheory.Fintype
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)
⊢ Eq.{u_1 + 1} (α := R) 2 0

Tactic:
rw [← add_eq_zero_iff_eq_neg, one_add_one_eq_two] at H

Premises used: add_eq_zero_iff_eq_neg, one_add_one_eq_two
-- Module: Mathlib.RingTheory.Fintype
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
⊢ 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

Premises used: Nat.prime_three, ZMod.ringEquivOfPrime, RingEquiv.symm
-- Module: Mathlib.RingTheory.Fintype
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)
⊢ Eq (α := ZMod 3) 2 0

Tactic:
simp only [map_ofNat, map_zero] at H

Premises used: map_ofNat, map_zero
-- Module: Mathlib.RingTheory.Fintype
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
⊢ Eq (α := ZMod 3) (↑2 : ZMod 3) 0

Tactic:
replace H : ((2 : ℕ) : ZMod 3) = 0 := H
-- Module: Mathlib.RingTheory.Fintype
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
⊢ Dvd.dvd (α := ℕ) 3 2

Tactic:
rw [natCast_eq_zero_iff] at H

Premises used: ZMod.natCast_eq_zero_iff
-- Module: Mathlib.RingTheory.Fintype
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 : Dvd.dvd (α := ℕ) 3 2
⊢ False

Tactic:
norm_num at H
-- Module: Mathlib.RingTheory.Fintype
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
⊢ 0 ∉ {1, -1}

Tactic:
simp
-- Module: Mathlib.RingTheory.Fintype
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Fintype M₀
⊢ Fintype.card.{u_1} M₀ˣ < Fintype.card M₀

Tactic:
Fintype.card_lt_of_injective_of_notMem Units.val Units.val_injective not_isUnit_zero

Premises used: Units.val, not_isUnit_zero, Fintype.card_lt_of_injective_of_notMem, Units.val_injective
-- Module: Mathlib.RingTheory.Fintype
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
have : ∀ (this : Fintype M₀), Nat.card.{u_1} M₀ˣ < Nat.card M₀
⊢ Nat.card.{u_1} M₀ˣ < Nat.card M₀

Tactic:
have : Fintype M₀ := Fintype.ofFinite M₀
-- Module: Mathlib.RingTheory.Fintype
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
this : Fintype M₀
⊢ Nat.card.{u_1} M₀ˣ < Nat.card M₀

Tactic:
simpa only [Fintype.card_eq_nat_card] using card_units_lt M₀

Premises used: card_units_lt, Fintype.card_eq_nat_card
-- Module: Mathlib.RingTheory.Fintype
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₀
neg : ∀ (h : ¬IsUnit a), orderOf a < Nat.card M₀
⊢ orderOf a < Nat.card M₀

Tactic:
by_cases h : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.RingTheory.Fintype
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
a : M₀
h : IsUnit a
pos : orderOf h.unit < Nat.card M₀
⊢ orderOf a < Nat.card M₀

Tactic:
rw [← h.unit_spec, orderOf_units]

Premises used: orderOf_units, IsUnit.unit_spec
-- Module: Mathlib.RingTheory.Fintype
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
a : M₀
h : IsUnit a
⊢ orderOf h.unit < Nat.card M₀

Tactic:
orderOf_le_card.trans_lt <| natCard_units_lt M₀

Premises used: orderOf_le_card, LE.le.trans_lt, natCard_units_lt
-- Module: Mathlib.RingTheory.Fintype
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
a : M₀
h : IsUnit a
⊢ orderOf h.unit < Nat.card M₀

Tactic:
exact orderOf_le_card.trans_lt <| natCard_units_lt M₀

Premises used: orderOf_le_card, LE.le.trans_lt, natCard_units_lt
-- Module: Mathlib.RingTheory.Fintype
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
a : M₀
h : ¬IsUnit a
neg : 0 < Nat.card M₀
⊢ orderOf a < Nat.card M₀

Tactic:
rw [orderOf_eq_zero_iff'.mpr fun n hn ha ↦ h <| IsUnit.of_pow_eq_one ha hn.ne']

Premises used: Iff.mpr, LT.lt.ne', orderOf_eq_zero_iff', IsUnit.of_pow_eq_one
-- Module: Mathlib.RingTheory.Fintype
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
a : M₀
h : ¬IsUnit a
⊢ 0 < Nat.card M₀

Tactic:
Nat.card_pos

Premises used: Nat.card_pos
-- Module: Mathlib.RingTheory.Fintype
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : Finite M₀
a : M₀
h : ¬IsUnit a
⊢ 0 < Nat.card M₀

Tactic:
exact Nat.card_pos

Premises used: Nat.card_pos
-- Module: Mathlib.RingTheory.Fintype
Goal:
n : ℕ
hn : 1 < n
a : ZMod n
⊢ orderOf a < n

Tactic:
have : NeZero n := ⟨Nat.ne_zero_of_lt hn⟩
  have : Nontrivial (ZMod n) := nontrivial_iff.mpr hn.ne'
  (orderOf_lt_card a).trans_eq <| Nat.card_zmod n

Premises used: Iff.mpr, orderOf_lt_card, NeZero.mk, LT.lt.trans_eq, LT.lt.ne', ZMod.nontrivial_iff, Nat.ne_zero_of_lt, Nat.card_zmod
-- Module: Mathlib.RingTheory.Flat.Basic
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)
⊢ Set.Finite (α := N ⊗[R] M) {x, y}

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
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)
have : ∀ (N' : Submodule R N) (Nfg : N'.FG) (sub : {x, y} ⊆ (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))), x = y
⊢ x = y

Tactic:
have ⟨N', Nfg, sub⟩ := Submodule.exists_fg_le_subset_range_rTensor_subtype {x, y} (by simp)
-- Module: Mathlib.RingTheory.Flat.Basic
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))
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
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := sub (.inl rfl)

Premises used: Or.inl, rfl