awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.CharacterModule
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 : LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B)
x : A ⊗[R] B
⊢ ∀ (x y : A ⊗[R] B),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
        (((liftAddHom (r • c).toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1) x :
          AddCircle (𝕜 := ℚ) 1)
        ((HSMul.hSMul (α := R) (β := CharacterModule (A ⊗[R] B)) ((RingHom.id R : (a : R) → R) r : R)
                (liftAddHom c.toAddMonoidHom ⋯) :
              (a : A ⊗[R] B) → AddCircle 1)
            x :
          AddCircle (𝕜 := ℚ) 1) →
      Eq (α := AddCircle (𝕜 := ℚ) 1)
          (((liftAddHom (r • c).toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1) y :
            AddCircle (𝕜 := ℚ) 1)
          ((HSMul.hSMul (α := R) (β := CharacterModule (A ⊗[R] B)) ((RingHom.id R : (a : R) → R) r : R)
                  (liftAddHom c.toAddMonoidHom ⋯) :
                (a : A ⊗[R] B) → AddCircle 1)
              y :
            AddCircle (𝕜 := ℚ) 1) →
        Eq (α := AddCircle (𝕜 := ℚ) 1)
          (((liftAddHom (r • c).toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1)
              (x + y) :
            AddCircle (𝕜 := ℚ) 1)
          ((HSMul.hSMul (α := R) (β := CharacterModule (A ⊗[R] B)) ((RingHom.id R : (a : R) → R) r : R)
                  (liftAddHom c.toAddMonoidHom ⋯) :
                (a : A ⊗[R] B) → AddCircle 1)
              (x + y) :
            AddCircle (𝕜 := ℚ) 1)

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.CharacterModule
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
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)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.CharacterModule
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
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:
congr(c $(TensorProduct.tmul_smul _ _ _)).symm

Premises used: Quotient.liftOn', congrArg, AddCon.liftOn, TensorProduct.tmul_smul, id, List.foldl, MulOpposite.unop, TensorProduct.tmul, Eq.symm, DFunLike.coe, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.Algebra.Module.CharacterModule
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
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:
exact congr(c $(TensorProduct.tmul_smul _ _ _)).symm

Premises used: congrArg, TensorProduct.tmul_smul, id, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Module.CharacterModule
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)
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' := ⋯, map_smul' := ⋯ } :
                  (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' := ⋯, map_smul' := ⋯ :
                      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)
⊢ {
      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) }

Tactic:
ext
-- Module: Mathlib.Algebra.Module.CharacterModule
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)
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' := ⋯, map_smul' := ⋯ } :
                (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' := ⋯, map_smul' := ⋯ : 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:
congr(c $(TensorProduct.tmul_smul _ _ _)).symm

Premises used: Quotient.liftOn', congrArg, AddCon.liftOn, TensorProduct.tmul_smul, id, List.foldl, TensorProduct.tmul, Eq.symm, DFunLike.coe, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.Algebra.Module.CharacterModule
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)
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' := ⋯, map_smul' := ⋯ } :
                (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' := ⋯, map_smul' := ⋯ : 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:
exact congr(c $(TensorProduct.tmul_smul _ _ _)).symm

Premises used: congrArg, TensorProduct.tmul_smul, id, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Module.CharacterModule
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
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)
⊢ Eq (α := CharacterModule (A ⊗[R] B) →ₗ[R] CharacterModule (A ⊗[R] B)) (uncurry ∘ₗ curry) LinearMap.id

Tactic:
ext _ z
-- Module: Mathlib.Algebra.Module.CharacterModule
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)

Tactic:
z.induction_on ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.Algebra.Module.CharacterModule
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)
      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:
aesop
-- Module: Mathlib.Algebra.Module.CharacterModule
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
⊢ ∀ (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:
aesop
-- Module: Mathlib.Algebra.Module.CharacterModule
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
⊢ ∀ (x_1 y : 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)
            x_1 :
          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 :
          AddCircle (𝕜 := ℚ) 1) →
      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)
              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)
              y :
            AddCircle (𝕜 := ℚ) 1) →
        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 + 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 + y) :
            AddCircle (𝕜 := ℚ) 1)

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.CharacterModule
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 (α :=
    LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B) →ₗ[R]
      LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B))
    (curry ∘ₗ uncurry) LinearMap.id

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.CharacterModule
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
f : A →ₗ[R] A'
⊢ Eq (α :=
    LinearMap.{uR, uR, u_1, uB} (RingHom.id R) A' (CharacterModule B) →ₗ[R]
      LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B))
    ((↑(LinearEquiv.symm homEquiv) : CharacterModule (A ⊗[R] B) →ₗ[R] A →ₗ[R] CharacterModule B) ∘ₗ
      dual (LinearMap.rTensor B f) ∘ₗ (↑homEquiv : (A' →ₗ[R] CharacterModule B) →ₗ[R] CharacterModule (A' ⊗[R] B)))
    (LinearMap.lcomp R (CharacterModule B) f)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.mk₂'ₛₗ, List.foldl, LinearMap.lcomp, LinearMap.flip, CharacterModule, FreeAddMonoid.sumAux, rfl, LinearMap.lcompₛₗ
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
n : ℕ
inl : Eq (α := AddCircle (𝕜 := ℚ) 1) ((int.divByNat 0 : (a : ℤ) → AddCircle 1) (↑0 : ℤ)) 0
inr : ∀ (h0 : n ≠ 0), Eq (α := AddCircle (𝕜 := ℚ) 1) ((int.divByNat n : (a : ℤ) → AddCircle 1) (↑n : ℤ)) 0
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((int.divByNat n : (a : ℤ) → AddCircle 1) (↑n : ℤ)) 0

Tactic:
obtain rfl | h0 := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((int.divByNat 0 : (a : ℤ) → AddCircle 1) (↑0 : ℤ)) 0

Tactic:
apply map_zero

Premises used: map_zero
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
n : ℕ
h0 : n ≠ 0
⊢ HSMul.hSMul (α := ℤ) (β := ℚ) 1 1 =
    (fun (x : ℚ) ↦ HSMul.hSMul (α := ℤ) ((LinearMap.id : (a : ℤ) → ℤ) (↑n : ℤ) : ℤ) x) (↑n : ℚ)⁻¹

Tactic:
simp [mul_inv_cancel₀ (Nat.cast_ne_zero (R := ℚ).mpr h0)]

Premises used: Iff.mpr, mul_inv_cancel₀, Nat.cast_ne_zero
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
n : ℕ
h0 : n ≠ 0
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((int.divByNat n : (a : ℤ) → AddCircle 1) (↑n : ℤ)) 0

Tactic:
exact (AddCircle.coe_eq_zero_iff _).mpr
    ⟨1, by simp [mul_inv_cancel₀ (Nat.cast_ne_zero (R := ℚ).mpr h0)]⟩

Premises used: Iff.mpr, AddCircle.coe_eq_zero_iff, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.CharacterModule
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 :
  ∀ (x : ℤ),
    x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔
      Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)}) x
⊢ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) = Ideal.span {(↑(addOrderOf a) : ℤ)}

Tactic:
ext1 x
-- Module: Mathlib.Algebra.Module.CharacterModule
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
h₃ h₄ : x • a = 0 ↔ x • a = 0
⊢ x ∈ LinearMap.ker (LinearMap.toSpanSingleton ℤ A a) ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)}) x

Tactic:
rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero, LinearMap.mem_ker,
      LinearMap.toSpanSingleton_apply]

Premises used: LinearMap.toSpanSingleton_apply, LinearMap.mem_ker, addOrderOf_dvd_iff_zsmul_eq_zero, Ideal.mem_span_singleton
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
⊢ Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)}))
    (((intSpanEquivQuotAddOrderOf a :
            ↥(ℤ ∙ a) ≃ₗ[ℤ] HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)})) :
          (a_1 : ↥(ℤ ∙ a)) → ℤ ⧸ Ideal.span {(↑(addOrderOf a) : ℤ)})
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submodule ℤ A) (ℤ ∙ a) x) a ⋯) :
      HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)}))
    (Submodule.Quotient.mk 1 : HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (Ideal.span {(↑(addOrderOf a) : ℤ)}))

Tactic:
(LinearEquiv.eq_symm_apply _).mp <| Subtype.ext (one_zsmul _).symm

Premises used: LinearEquiv.eq_symm_apply, one_zsmul, Iff.mp, Eq.symm, Subtype.ext
-- Module: Mathlib.Algebra.Module.CharacterModule
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
neg :
  ∀ (h : ¬addOrderOf a = 0),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
      ((AddMonoidHom.toIntLinearMap (int.divByNat (addOrderOf a)) : (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

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Module.CharacterModule
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
pos₂ pos₃ : Eq (α := AddCircle (𝕜 := ℚ) 1) 0 0
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((AddMonoidHom.toIntLinearMap (int.divByNat 2) : (a : ℤ) → AddCircle 1) (↑(addOrderOf a) : ℤ)) 0

Tactic:
rw [h, Nat.cast_zero, map_zero]

Premises used: map_zero, Nat.cast_zero
-- Module: Mathlib.Algebra.Module.CharacterModule
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 (addOrderOf a)) : (a : ℤ) → AddCircle 1) (↑(addOrderOf a) : ℤ)) 0

Tactic:
apply CharacterModule.int.divByNat_self

Premises used: CharacterModule.int.divByNat_self
-- Module: Mathlib.Algebra.Module.CharacterModule
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)
⊢ ∃ (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

Premises used: LinearMap.toAddMonoidHom_coe, AddCircle.coe_eq_zero_iff, CharacterModule.ofSpanSingleton, LinearMap.comp_apply, LinearMap.toSpanSingleton_apply_one, CharacterModule.int.divByNat, Submodule.liftQSpanSingleton_apply, AddMonoidHom.coe_toIntLinearMap, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
h : ∃ (n : ℤ), HSMul.hSMul (β := ℚ) n 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹
rcases : ∀ (n : ℤ) (hn : HSMul.hSMul (β := ℚ) n 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹), a = 0
⊢ a = 0

Tactic:
rcases h with ⟨n, hn⟩
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
A : Type uA
inst : AddCommGroup A
a : A
n : ℤ
hn : HSMul.hSMul (β := ℚ) n 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹
⊢ (HSMul.hSMul (β := ℚ) n 1).den = Rat.den (↑(if addOrderOf a = 0 then 2 else addOrderOf a) : ℚ)⁻¹

Tactic:
apply_fun Rat.den at hn

Premises used: Rat.den