awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
inst_4 : Module R A
inst_5 : Module R A'
inst_6 : Module R B
c c' : LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B)
x : A ⊗[R] B
refine_1 :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((liftAddHom (c + c').toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1) 0)
    ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom ⋯) (liftAddHom c'.toAddMonoidHom ⋯) :
        (a : A ⊗[R] B) → AddCircle 1)
      0)
refine_2 :
  ∀ (x : A) (y : B),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
      (((liftAddHom (c + c').toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1)
          (x ⊗ₜ[R] y) :
        AddCircle (𝕜 := ℚ) 1)
      ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom ⋯) (liftAddHom c'.toAddMonoidHom ⋯) :
            (a : A ⊗[R] B) → AddCircle 1)
          (x ⊗ₜ[R] y) :
        AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((liftAddHom (c + c').toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1) x :
      AddCircle (𝕜 := ℚ) 1)
    ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom ⋯) (liftAddHom c'.toAddMonoidHom ⋯) :
          (a : A ⊗[R] B) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)
have refine_3 : ∀ (x y : A ⊗[R] B),
  Eq (α := AddCircle (𝕜 := ℚ) 1)
      (((liftAddHom (c + c').toAddMonoidHom sorry : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1) x :
        AddCircle (𝕜 := ℚ) 1)
      ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom sorry) (liftAddHom c'.toAddMonoidHom sorry) :
            (a : A ⊗[R] B) → AddCircle 1)
          x :
        AddCircle (𝕜 := ℚ) 1) →
    Eq (α := AddCircle (𝕜 := ℚ) 1)
        (((liftAddHom (c + c').toAddMonoidHom sorry : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1) y :
          AddCircle (𝕜 := ℚ) 1)
        ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom sorry) (liftAddHom c'.toAddMonoidHom sorry) :
              (a : A ⊗[R] B) → AddCircle 1)
            y :
          AddCircle (𝕜 := ℚ) 1) →
      Eq (α := AddCircle (𝕜 := ℚ) 1)
        (((liftAddHom (c + c').toAddMonoidHom sorry : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1)
            (x + y) :
          AddCircle (𝕜 := ℚ) 1)
        ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom sorry) (liftAddHom c'.toAddMonoidHom sorry) :
              (a : A ⊗[R] B) → AddCircle 1)
            (x + y) :
          AddCircle (𝕜 := ℚ) 1)
Tactic: refine x.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
inst_4 : Module R A
inst_5 : Module R A'
inst_6 : Module R B
c : CharacterModule (A ⊗[R] B)
r : R
a : A
⊢ AddMonoidHom.comp c (↑((mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) (r • a) : B →ₗ[R] A ⊗[R] B) : B →+ A ⊗[R] B) =
    HSMul.hSMul (α := R) (β := CharacterModule B) ((RingHom.id R : (a : R) → R) r : R)
      (AddMonoidHom.comp c (↑((mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) a : B →ₗ[R] A ⊗[R] B) : B →+ A ⊗[R] B))
have h : ∀ (x : B),
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddMonoidHom.comp c (↑((mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) (r • a) : B →ₗ[R] A ⊗[R] B) : B →+ A ⊗[R] B) :
            B →+ AddCircle (𝕜 := ℚ) 1) :
          (a : B) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)
    ((HSMul.hSMul (α := R) (β := CharacterModule B) ((RingHom.id R : (a : R) → R) r : R)
            (AddMonoidHom.comp c (↑((mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) a : B →ₗ[R] A ⊗[R] B) : B →+ A ⊗[R] B)) :
          (a : B) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
inst_4 : Module R A
inst_5 : Module R A'
inst_6 : Module R B
r : R
c : CharacterModule (A ⊗[R] B)
⊢ {
      toFun := fun (x : A) ↦
        AddMonoidHom.comp (r • c) (↑((mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) x : B →ₗ[R] A ⊗[R] B) : B →+ A ⊗[R] B),
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B))
      ((RingHom.id R : (a : R) → R) r : R)
      {
        toFun := fun (x : A) ↦
          AddMonoidHom.comp c (↑((mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) x : B →ₗ[R] A ⊗[R] B) : B →+ A ⊗[R] B),
        map_add' := ⋯, map_smul' := ⋯ : LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B) }
have h : ∀ (x : A) (x_1 : B),
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((({
                  toFun := fun (x : A) ↦
                    AddMonoidHom.comp (r • c)
                      (↑((mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) x : B →ₗ[R] A ⊗[R] B) : B →+ A ⊗[R] B),
                  map_add' := sorry, map_smul' := sorry } :
                (a : A) → CharacterModule B)
              x :
            CharacterModule B) :
          (a : B) → AddCircle 1)
        x_1 :
      AddCircle (𝕜 := ℚ) 1)
    ((((HSMul.hSMul (α := R) (β := LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B))
                  ((RingHom.id R : (a : R) → R) r : R)
                  {
                    toFun := fun (x : A) ↦
                      AddMonoidHom.comp c
                        (↑((mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) x : B →ₗ[R] A ⊗[R] B) : B →+ A ⊗[R] B),
                    map_add' := sorry, map_smul' := sorry : LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B) } :
                (a : A) → CharacterModule B)
              x :
            CharacterModule B) :
          (a : B) → AddCircle 1)
        x_1 :
      AddCircle (𝕜 := ℚ) 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
inst_4 : Module R A
inst_5 : Module R A'
inst_6 : Module R B
⊢ Eq (α := CharacterModule (A ⊗[R] B) →ₗ[R] CharacterModule (A ⊗[R] B)) (uncurry ∘ₗ curry) LinearMap.id
have h : ∀ (x : CharacterModule (A ⊗[R] B)) (z : A ⊗[R] B),
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((uncurry ∘ₗ curry : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x :
            CharacterModule (A ⊗[R] B)) :
          (a : A ⊗[R] B) → AddCircle 1)
        z :
      AddCircle (𝕜 := ℚ) 1)
    ((((LinearMap.id : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x : CharacterModule (A ⊗[R] B)) :
          (a : A ⊗[R] B) → AddCircle 1)
        z :
      AddCircle (𝕜 := ℚ) 1)
Tactic: ext _ z
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
inst_4 : Module R A
inst_5 : Module R A'
inst_6 : Module R B
x : CharacterModule (A ⊗[R] B)
z : A ⊗[R] B
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((uncurry ∘ₗ curry : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x :
            CharacterModule (A ⊗[R] B)) :
          (a : A ⊗[R] B) → AddCircle 1)
        z :
      AddCircle (𝕜 := ℚ) 1)
    ((((LinearMap.id : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x : CharacterModule (A ⊗[R] B)) :
          (a : A ⊗[R] B) → AddCircle 1)
        z :
      AddCircle (𝕜 := ℚ) 1)
have h : Eq (α := AddCircle (𝕜 := ℚ) 1)
  ((((uncurry ∘ₗ curry : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x :
        CharacterModule (A ⊗[R] B)) :
      (a : A ⊗[R] B) → AddCircle 1)
    0)
  ((((LinearMap.id : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x : CharacterModule (A ⊗[R] B)) :
      (a : A ⊗[R] B) → AddCircle 1)
    0)
Tactic: refine z.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
inst_4 : Module R A
inst_5 : Module R A'
inst_6 : Module R B
x : CharacterModule (A ⊗[R] B)
z : A ⊗[R] B
h :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((uncurry ∘ₗ curry : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x :
          CharacterModule (A ⊗[R] B)) :
        (a : A ⊗[R] B) → AddCircle 1)
      0)
    ((((LinearMap.id : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x : CharacterModule (A ⊗[R] B)) :
        (a : A ⊗[R] B) → AddCircle 1)
      0)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((uncurry ∘ₗ curry : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x :
            CharacterModule (A ⊗[R] B)) :
          (a : A ⊗[R] B) → AddCircle 1)
        z :
      AddCircle (𝕜 := ℚ) 1)
    ((((LinearMap.id : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x : CharacterModule (A ⊗[R] B)) :
          (a : A ⊗[R] B) → AddCircle 1)
        z :
      AddCircle (𝕜 := ℚ) 1)
have h₁ : ∀ (x_1 : A) (y : B),
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((uncurry ∘ₗ curry : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x :
            CharacterModule (A ⊗[R] B)) :
          (a : A ⊗[R] B) → AddCircle 1)
        (x_1 ⊗ₜ[R] y) :
      AddCircle (𝕜 := ℚ) 1)
    ((((LinearMap.id : (a : CharacterModule (A ⊗[R] B)) → CharacterModule (A ⊗[R] B)) x : CharacterModule (A ⊗[R] B)) :
          (a : A ⊗[R] B) → AddCircle 1)
        (x_1 ⊗ₜ[R] y) :
      AddCircle (𝕜 := ℚ) 1)
Tactic: refine z.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
n : ℕ
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((int.divByNat n : (a : ℤ) → AddCircle 1) (↑n : ℤ)) 0
have inl : Eq (α := AddCircle (𝕜 := ℚ) 1) ((int.divByNat 0 : (a : ℤ) → AddCircle 1) (↑0 : ℤ)) 0
Tactic: obtain rfl | h0 := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
n : ℕ
inl : Eq (α := AddCircle (𝕜 := ℚ) 1) ((int.divByNat 0 : (a : ℤ) → AddCircle 1) (↑0 : ℤ)) 0
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((int.divByNat n : (a : ℤ) → AddCircle 1) (↑n : ℤ)) 0
have inr : ∀ (h0 : n ≠ 0), Eq (α := AddCircle (𝕜 := ℚ) 1) ((int.divByNat n : (a : ℤ) → AddCircle 1) (↑n : ℤ)) 0
Tactic: obtain rfl | h0 := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
a : A
⊢ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) = Ideal.span {(↑(addOrderOf a) : ℤ)}
have h : ∀ (x : ℤ),
  x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)}) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
a : A
x : ℤ
⊢ x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)}) x
have h : x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔ (↑(addOrderOf a) : ℤ) ∣ x
Tactic: rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero, LinearMap.mem_ker,
      LinearMap.toSpanSingleton_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
a : A
x : ℤ
h : x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔ (↑(addOrderOf a) : ℤ) ∣ x
⊢ x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)}) x
have h₁ : x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔ x • a = 0
Tactic: rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero, LinearMap.mem_ker,
      LinearMap.toSpanSingleton_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
a : A
x : ℤ
h : x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔ (↑(addOrderOf a) : ℤ) ∣ x
h₁ : x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔ x • a = 0
⊢ x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)}) x
have h₂ : Eq (α := A) ((LinearMap.toSpanSingleton ℤ A a : (a : ℤ) → A) x : A) (0 : A) ↔ x • a = 0
Tactic: rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero, LinearMap.mem_ker,
      LinearMap.toSpanSingleton_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
a : A
x : ℤ
h : x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔ (↑(addOrderOf a) : ℤ) ∣ x
h₁ : x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔ x • a = 0
h₂ : Eq (α := A) ((LinearMap.toSpanSingleton ℤ A a : (a : ℤ) → A) x : A) (0 : A) ↔ x • a = 0
⊢ x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)}) x
have h₃ : x • a = 0 ↔ x • a = 0
Tactic: rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero, LinearMap.mem_ker,
      LinearMap.toSpanSingleton_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
a : A
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((AddMonoidHom.toIntLinearMap (int.divByNat (if addOrderOf a = 0 then 2 else addOrderOf a)) : (a : ℤ) → AddCircle 1)
      (↑(addOrderOf a) : ℤ))
    0
have pos : ∀ (h : addOrderOf a = 0),
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) (↑(addOrderOf a) : ℤ)) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
a : A
pos :
  ∀ (h : addOrderOf a = 0),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
      ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) (↑(addOrderOf a) : ℤ)) 0
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((AddMonoidHom.toIntLinearMap (int.divByNat (if addOrderOf a = 0 then 2 else addOrderOf a)) : (a : ℤ) → AddCircle 1)
      (↑(addOrderOf a) : ℤ))
    0
have neg : ∀ (h : ¬addOrderOf a = 0),
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((AddMonoidHom.toIntLinearMap (int.divByNat (addOrderOf a)) : (a : ℤ) → AddCircle 1) (↑(addOrderOf a) : ℤ)) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
a : A
h : addOrderOf a = 0
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) (↑(addOrderOf a) : ℤ)) 0
have pos : Eq (α := AddCircle (𝕜 := ℚ) 1) ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) (↑0 : ℤ)) 0
Tactic: rw [h, Nat.cast_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
a : A
h : addOrderOf a = 0
pos : Eq (α := AddCircle (𝕜 := ℚ) 1) ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) (↑0 : ℤ)) 0
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) (↑(addOrderOf a) : ℤ)) 0
have pos₁ : Eq (α := AddCircle (𝕜 := ℚ) 1) ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) 0) 0
Tactic: rw [h, Nat.cast_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
B : Type uB
inst_3 : AddCommGroup B
a : A
h : addOrderOf a = 0
pos : Eq (α := AddCircle (𝕜 := ℚ) 1) ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) (↑0 : ℤ)) 0
pos₁ : Eq (α := AddCircle (𝕜 := ℚ) 1) ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) 0) 0
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) (↑(addOrderOf a) : ℤ)) 0
have pos₂ : Eq (α := AddCircle (𝕜 := ℚ) 1) 0 0
Tactic: rw [h, Nat.cast_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (hypothesis)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
h :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((ofSpanSingleton a : CharacterModule ↥(ℤ ∙ a)) : (a : ↥(ℤ ∙ a)) → AddCircle 1)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule ℤ A) (ℤ ∙ a) x) a ⋯) :
      AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)
⊢ a = 0
have h₁ : ∃ (n : ℤ), HSMul.hSMul (β := ℚ) n 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹
Tactic: erw [ofSpanSingleton, LinearMap.toAddMonoidHom_coe, LinearMap.comp_apply,
     intSpanEquivQuotAddOrderOf_apply_self, Submodule.liftQSpanSingleton_apply,
    AddMonoidHom.coe_toIntLinearMap, int.divByNat, LinearMap.toSpanSingleton_apply_one,
    AddCircle.coe_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
h : ∃ (n : ℤ), HSMul.hSMul (β := ℚ) n 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹
⊢ a = 0
have rcases : ∀ (n : ℤ) (hn : HSMul.hSMul (β := ℚ) n 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹), a = 0
Tactic: rcases h with ⟨n, hn⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (hypothesis)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
hn : HSMul.hSMul (β := ℚ) n 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹
⊢ a = 0
have hn₁ : (HSMul.hSMul (β := ℚ) n 1).den = Rat.den (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹
Tactic: apply_fun Rat.den at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
hn : (HSMul.hSMul (β := ℚ) n 1).den = Rat.den (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹
⊢ a = 0
have rw : ∀ (hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a), a = 0
Tactic: rw [zsmul_one, Rat.den_intCast, Rat.inv_natCast_den_of_pos] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
hn : (HSMul.hSMul (β := ℚ) n 1).den = Rat.den (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹
rw : ∀ (hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a), a = 0
⊢ a = 0
have rw₁ : ∀ (hn : 1 = Rat.den (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹),
  0 < if addOrderOf a = 0 then 2 else addOrderOf a
Tactic: rw [zsmul_one, Rat.den_intCast, Rat.inv_natCast_den_of_pos] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a
⊢ a = 0
have pos : addOrderOf a = 0 → ∀ (hn : Eq (α := ℕ) 1 2), a = 0
Tactic: split_ifs at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a
pos : addOrderOf a = 0 → ∀ (hn : Eq (α := ℕ) 1 2), a = 0
⊢ a = 0
have neg : ¬addOrderOf a = 0 → ∀ (hn : 1 = addOrderOf a), a = 0
Tactic: split_ifs at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
h : ¬addOrderOf a = 0
hn : 1 = addOrderOf a
⊢ a = 0
have neg : ∀ (hn : addOrderOf a = 1), a = 0
Tactic: rwa [eq_comm, AddMonoid.addOrderOf_eq_one_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
h : ¬addOrderOf a = 0
hn : 1 = addOrderOf a
neg : ∀ (hn : addOrderOf a = 1), a = 0
⊢ a = 0
have neg₁ : ∀ (hn : a = 0), a = 0
Tactic: rwa [eq_comm, AddMonoid.addOrderOf_eq_one_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
ne_zero : a ≠ 0
c : CharacterModule A
hc :
  Eq (α := CharacterModule ↥(ℤ ∙ a))
    ((dual (Submodule.subtype (ℤ ∙ a)) : (a_1 : CharacterModule A) → CharacterModule ↥(ℤ ∙ a)) c :
      CharacterModule ↥(ℤ ∙ a))
    (ofSpanSingleton a : CharacterModule ↥(ℤ ∙ a))
h : Eq (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1) (0 : AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((ofSpanSingleton a : CharacterModule ↥(ℤ ∙ a)) : (a : ↥(ℤ ∙ a)) → AddCircle 1)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule ℤ A) (ℤ ∙ a) x) a ⋯) :
      AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)
have rwa : Eq (α := AddCircle (𝕜 := ℚ) 1)
  ((((dual (Submodule.subtype (ℤ ∙ a)) : (a_1 : CharacterModule A) → CharacterModule ↥(ℤ ∙ a)) c :
          CharacterModule ↥(ℤ ∙ a)) :
        (a : ↥(ℤ ∙ a)) → AddCircle 1)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule ℤ A) (ℤ ∙ a) x) a sorry) :
    AddCircle (𝕜 := ℚ) 1)
  (0 : AddCircle (𝕜 := ℚ) 1)
Tactic: rwa [← hc]
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
A : Type uA
inst : AddCommGroup A
a : A
h :
  ∀ (c : CharacterModule A),
    Eq (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1) (0 : AddCircle (𝕜 := ℚ) 1)
⊢ a = 0
have contrapose! : ∀ (h : a ≠ 0),
  ∃ (c : CharacterModule A),
    Ne (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1) (0 : AddCircle (𝕜 := ℚ) 1)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
h :
  Function.Surjective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
a : A
h0 : Eq.{u_1 + 1} (α := A') ((f : (a : A) → A') a : A') (0 : A')
c : CharacterModule A
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((c : (a : A) → AddCircle 1) a : AddCircle (𝕜 := ℚ) 1) (0 : AddCircle (𝕜 := ℚ) 1)
have obtain : ∀ (c : CharacterModule A'),
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual f : (a : CharacterModule A') → CharacterModule A) c : CharacterModule A) : (a : A) → AddCircle 1) a :
      AddCircle (𝕜 := ℚ) 1)
    (0 : AddCircle (𝕜 := ℚ) 1)
Tactic: obtain ⟨c, rfl⟩ := h c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
A' : Type u_1
inst_2 : AddCommGroup A'
inst_3 : Module R A
inst_4 : Module R A'
f : A →ₗ[R] A'
hf :
  Function.Injective.{u_1 + 1, uA + 1} (α := CharacterModule A') (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule A') → CharacterModule A)
⊢ Function.Surjective.{uA + 1, u_1 + 1} (α := A) (β := A') (⇑f : (a : A) → A')
have rw : Nonempty.{u_1 + 1} (Unique (A' ⧸ f.range))
Tactic: rw [← LinearMap.range_eq_top, ← Submodule.unique_quotient_iff_eq_top]