awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
have succ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = f.iterateMapComap i (n + 1 + 1) K
Tactic: rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
succ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = f.iterateMapComap i (n + 1 + 1) K
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
have succ₁ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
Tactic: rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
succ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = f.iterateMapComap i (n + 1 + 1) K
succ₁ :
  (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
have succ₂ : ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K =
  (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
Tactic: rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
succ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = f.iterateMapComap i (n + 1 + 1) K
succ₁ :
  (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₂ :
  ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K =
    (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
have succ₃ : Eq (α := Submodule R N)
  (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K)
  (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K)
Tactic: rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
succ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = f.iterateMapComap i (n + 1 + 1) K
succ₁ :
  (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₂ :
  ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K =
    (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₃ :
  Eq (α := Submodule R N)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K)
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
have succ₄ : comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
  ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K
Tactic: rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
succ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = f.iterateMapComap i (n + 1 + 1) K
succ₁ :
  (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₂ :
  ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K =
    (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₃ :
  Eq (α := Submodule R N)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K)
succ₄ :
  comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
    ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
have succ₅ : comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
  comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K))
Tactic: rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
succ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = f.iterateMapComap i (n + 1 + 1) K
succ₁ :
  (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₂ :
  ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K =
    (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₃ :
  Eq (α := Submodule R N)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K)
succ₄ :
  comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
    ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K
succ₅ :
  comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
    comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K))
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
have succ₆ : comap f (map i (f.iterateMapComap i n K)) = comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K))
Tactic: rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
succ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = f.iterateMapComap i (n + 1 + 1) K
succ₁ :
  (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₂ :
  ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K =
    (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₃ :
  Eq (α := Submodule R N)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K)
succ₄ :
  comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
    ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K
succ₅ :
  comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
    comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K))
succ₆ :
  comap f (map i (f.iterateMapComap i n K)) = comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K))
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
have succ₇ : comap f (map i (f.iterateMapComap i n K)) = comap f (map i (f.iterateMapComap i (n + 1) K))
Tactic: rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
succ : (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = f.iterateMapComap i (n + 1 + 1) K
succ₁ :
  (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K = (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₂ :
  ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K =
    (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1 + 1] K
succ₃ :
  Eq (α := Submodule R N)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n]) K)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K)
succ₄ :
  comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
    ((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1]) K
succ₅ :
  comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)) =
    comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K))
succ₆ :
  comap f (map i (f.iterateMapComap i n K)) = comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K))
succ₇ : comap f (map i (f.iterateMapComap i n K)) = comap f (map i (f.iterateMapComap i (n + 1) K))
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
have succ₈ : comap f (map i (f.iterateMapComap i (n + 1) K)) = comap f (map i (f.iterateMapComap i (n + 1) K))
Tactic: rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
⊢ f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
have zero : f.iterateMapComap i 0 K = f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
Tactic: induction n with
  | zero =>
    contrapose! heq
    induction m with
    | zero => exact heq
    | succ m ih =>
      rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']
      exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))
  | succ n ih =>
    rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
n : ℕ
zero : f.iterateMapComap i 0 K = f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
⊢ f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
have succ : ∀ (n : ℕ) (ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K),
  f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K
Tactic: induction n with
  | zero =>
    contrapose! heq
    induction m with
    | zero => exact heq
    | succ m ih =>
      rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']
      exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))
  | succ n ih =>
    rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
⊢ f.ker ≤ K
have rw : f.ker ≤ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
Tactic: rw [show K = _ from f.iterateMapComap_eq_succ i K m heq hf hi 0]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ Subsingleton.{u_3 + 1} ↥p ↔ p = ⊥
have rw : (∀ (x y : ↥p), x = y) ↔ ∀ x ∈ p, x = 0
Tactic: rw [subsingleton_iff, Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ Nontrivial.{u_3} ↥p ↔ p ≠ ⊥
have rw : p = ⊥ ↔ ¬Nontrivial.{u_3} ↥p
Tactic: rw [iff_not_comm, not_nontrivial_iff_subsingleton, subsingleton_iff_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
rw : p = ⊥ ↔ ¬Nontrivial.{u_3} ↥p
⊢ Nontrivial.{u_3} ↥p ↔ p ≠ ⊥
have rw₁ : p = ⊥ ↔ Subsingleton.{u_3 + 1} ↥p
Tactic: rw [iff_not_comm, not_nontrivial_iff_subsingleton, subsingleton_iff_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
rw : p = ⊥ ↔ ¬Nontrivial.{u_3} ↥p
rw₁ : p = ⊥ ↔ Subsingleton.{u_3 + 1} ↥p
⊢ Nontrivial.{u_3} ↥p ↔ p ≠ ⊥
have rw₂ : p = ⊥ ↔ p = ⊥
Tactic: rw [iff_not_comm, not_nontrivial_iff_subsingleton, subsingleton_iff_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ (↑p : Set M) = Set.univ ↔ p = ⊤
have rw : p = ⊤ ↔ (↑p : Set M) = Set.univ
Tactic: rw [iff_comm, ← SetLike.coe_set_eq, top_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
rw : p = ⊤ ↔ (↑p : Set M) = Set.univ
⊢ (↑p : Set M) = Set.univ ↔ p = ⊤
have rw₁ : (↑p : Set M) = (↑⊤ : Set M) ↔ (↑p : Set M) = Set.univ
Tactic: rw [iff_comm, ← SetLike.coe_set_eq, top_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
rw : p = ⊤ ↔ (↑p : Set M) = Set.univ
rw₁ : (↑p : Set M) = (↑⊤ : Set M) ↔ (↑p : Set M) = Set.univ
⊢ (↑p : Set M) = Set.univ ↔ p = ⊤
have rw₂ : (↑p : Set M) = Set.univ ↔ (↑p : Set M) = Set.univ
Tactic: rw [iff_comm, ← SetLike.coe_set_eq, top_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ (↑(s.inf p) : Set M) = ⋂ i ∈ s, (↑(p i) : Set M)
have refine_1 : (↑(Finset.inf ∅ p) : Set M) = ⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(p i) : Set M)
Tactic: refine s.induction_on ?_ fun i s _ ih ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
refine_1 : (↑(Finset.inf ∅ p) : Set M) = ⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(p i) : Set M)
⊢ (↑(s.inf p) : Set M) = ⋂ i ∈ s, (↑(p i) : Set M)
have refine_2 : ∀ (i : ι) (s : Finset ι),
  i ∉ s →
    ∀ (ih : (↑(s.inf p) : Set M) = ⋂ i ∈ s, (↑(p i) : Set M)),
      (↑((insert i s).inf p) : Set M) = ⋂ i_1 ∈ insert i s, (↑(p i_1) : Set M)
Tactic: refine s.induction_on ?_ fun i s _ ih ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
s_1 : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
h : i ∉ s
ih : (↑(s.inf p) : Set M) = ⋂ i ∈ s, (↑(p i) : Set M)
⊢ (↑((insert i s).inf p) : Set M) = ⋂ i_1 ∈ insert i s, (↑(p i_1) : Set M)
have refine_2 : (↑(p i) : Set M) ∩ ⋂ i ∈ s, (↑(p i) : Set M) = ⋂ i_1 ∈ insert i s, (↑(p i_1) : Set M)
Tactic: rw [Finset.inf_insert, coe_inf, ih]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), p i) x ↔ ∀ (i : ι), x ∈ p i
have rw : (∀ (i : ι), x ∈ (↑(p i) : Set M)) ↔ ∀ (i : ι), x ∈ p i
Tactic: rw [← SetLike.mem_coe, coe_iInf, Set.mem_iInter]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
have this : S ≤ S ⊔ T
Tactic: have : S ≤ S ⊔ T := le_sup_left
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
have this₁ : (Preorder.toLE : LE (Submodule R M)).1 S (S ⊔ T)
Tactic: rw [LE.le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
have this : T ≤ S ⊔ T
Tactic: have : T ≤ S ⊔ T := le_sup_right
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
have this₁ : (Preorder.toLE : LE (Submodule R M)).1 T (S ⊔ T)
Tactic: rw [LE.le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (goal)
Goal:
R' : Type u_4
M' : Type u_5
inst : Ring R'
inst_1 : AddCommGroup M'
inst_2 : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s - t ∈ S ⊔ T
have rw : s + -t ∈ S ⊔ T
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
have this : s ≤ sSup S
Tactic: have := le_sSup hs
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Lattice (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
have this₁ : (Preorder.toLE : LE (Submodule R M)).1 s (sSup S)
Tactic: rw [LE.le] at this
Cleared hypotheses: this