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
f : A →ₗ[R] B
⊢ ∀ (x y : CharacterModule B),
    AddMonoidHom.comp (x + y) f.toAddMonoidHom =
      AddMonoidHom.comp x f.toAddMonoidHom + AddMonoidHom.comp y f.toAddMonoidHom

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] B
r : R
c : CharacterModule B
h :
  ∀ (x : A),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
      ((AddMonoidHom.comp (r • c) f.toAddMonoidHom : (a : A) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
      ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (AddMonoidHom.comp c f.toAddMonoidHom) :
            (a : A) → AddCircle 1)
          x :
        AddCircle (𝕜 := ℚ) 1)
⊢ AddMonoidHom.comp (r • c) f.toAddMonoidHom =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (AddMonoidHom.comp c f.toAddMonoidHom)

Tactic:
ext 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
inst_4 : Module R A
inst_5 : Module R A'
inst_6 : Module R B
f : A →ₗ[R] B
r : R
c : CharacterModule B
x : A
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((AddMonoidHom.comp (r • c) f.toAddMonoidHom : (a : A) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (AddMonoidHom.comp c f.toAddMonoidHom) :
          (a : A) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
congr(c $(f.map_smul r x)).symm

Premises used: congrArg, id, LinearMap.map_smul, MulOpposite.unop, 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
f : A →ₗ[R] B
r : R
c : CharacterModule B
x : A
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((AddMonoidHom.comp (r • c) f.toAddMonoidHom : (a : A) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (AddMonoidHom.comp c f.toAddMonoidHom) :
          (a : A) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
exact congr(c $(f.map_smul r x)).symm

Premises used: congrArg, id, LinearMap.map_smul, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
h :
  ∀ (f : CharacterModule B) (x : A),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
      ((((dual 0 : (a : CharacterModule B) → CharacterModule A) f : CharacterModule A) : (a : A) → AddCircle 1) x :
        AddCircle (𝕜 := ℚ) 1)
      (((((0 : LinearMap.{uR, uR, uB, uA} (RingHom.id R) (CharacterModule B) (CharacterModule A)) :
                  (a : CharacterModule B) → CharacterModule A)
                f :
              CharacterModule A) :
            (a : A) → AddCircle 1)
          x :
        AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := LinearMap.{uR, uR, uB, uA} (RingHom.id R) (CharacterModule B) (CharacterModule A)) (dual 0) 0

Tactic:
ext f
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
f : CharacterModule B
x : A
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual 0 : (a : CharacterModule B) → CharacterModule A) f : CharacterModule A) : (a : A) → AddCircle 1) x :
      AddCircle (𝕜 := ℚ) 1)
    (((((0 : LinearMap.{uR, uR, uB, uA} (RingHom.id R) (CharacterModule B) (CharacterModule A)) :
                (a : CharacterModule B) → CharacterModule A)
              f :
            CharacterModule A) :
          (a : A) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
map_zero f

Premises used: map_zero
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
f : CharacterModule B
x : A
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual 0 : (a : CharacterModule B) → CharacterModule A) f : CharacterModule A) : (a : A) → AddCircle 1) x :
      AddCircle (𝕜 := ℚ) 1)
    (((((0 : LinearMap.{uR, uR, uB, uA} (RingHom.id R) (CharacterModule B) (CharacterModule A)) :
                (a : CharacterModule B) → CharacterModule A)
              f :
            CharacterModule A) :
          (a : A) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
exact map_zero f

Premises used: map_zero
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
C : Type u_2
inst_5 : AddCommGroup C
inst_6 : Module R C
f : A →ₗ[R] B
g : B →ₗ[R] C
h :
  ∀ (x : CharacterModule C) (x_1 : A),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
      ((((dual (g ∘ₗ f) : (a : CharacterModule C) → CharacterModule A) x : CharacterModule A) : (a : A) → AddCircle 1)
          x_1 :
        AddCircle (𝕜 := ℚ) 1)
      ((((dual f ∘ₗ dual g : (a : CharacterModule C) → CharacterModule A) x : CharacterModule A) :
            (a : A) → AddCircle 1)
          x_1 :
        AddCircle (𝕜 := ℚ) 1)
⊢ dual (g ∘ₗ f) = dual f ∘ₗ dual g

Tactic:
ext
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
C : Type u_2
inst_5 : AddCommGroup C
inst_6 : Module R C
f : A →ₗ[R] B
g : B →ₗ[R] C
x : CharacterModule C
x_1 : A
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual (g ∘ₗ f) : (a : CharacterModule C) → CharacterModule A) x : CharacterModule A) : (a : A) → AddCircle 1)
        x_1 :
      AddCircle (𝕜 := ℚ) 1)
    ((((dual f ∘ₗ dual g : (a : CharacterModule C) → CharacterModule A) x : CharacterModule A) : (a : A) → AddCircle 1)
        x_1 :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
f : A →ₗ[R] B
hf : Function.Surjective.{uA + 1, uB + 1} (α := A) (β := B) (⇑f : (a : A) → B)
φ ψ : CharacterModule B
eq :
  Eq.{uA + 1} (α := CharacterModule A) ((dual f : (a : CharacterModule B) → CharacterModule A) φ : CharacterModule A)
    ((dual f : (a : CharacterModule B) → CharacterModule A) ψ : CharacterModule A)
h :
  ∀ (x : B),
    Eq (α := AddCircle (𝕜 := ℚ) 1) ((φ : (a : B) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
      ((ψ : (a : B) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
⊢ φ = ψ

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
f : A →ₗ[R] B
hf : Function.Surjective.{uA + 1, uB + 1} (α := A) (β := B) (⇑f : (a : A) → B)
φ ψ : CharacterModule B
eq :
  Eq.{uA + 1} (α := CharacterModule A) ((dual f : (a : CharacterModule B) → CharacterModule A) φ : CharacterModule A)
    ((dual f : (a : CharacterModule B) → CharacterModule A) ψ : CharacterModule A)
x : B
h :
  ∀ (y : A),
    Eq (α := AddCircle (𝕜 := ℚ) 1) ((φ : (a : B) → AddCircle 1) ((f : (a : A) → B) y) : AddCircle (𝕜 := ℚ) 1)
      ((ψ : (a : B) → AddCircle 1) ((f : (a : A) → B) y) : AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((φ : (a : B) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
    ((ψ : (a : B) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)

Tactic:
obtain ⟨y, rfl⟩ := hf x

Premises used: rfl
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
f : A →ₗ[R] B
hf : Function.Surjective.{uA + 1, uB + 1} (α := A) (β := B) (⇑f : (a : A) → B)
φ ψ : CharacterModule B
eq :
  Eq.{uA + 1} (α := CharacterModule A) ((dual f : (a : CharacterModule B) → CharacterModule A) φ : CharacterModule A)
    ((dual f : (a : CharacterModule B) → CharacterModule A) ψ : CharacterModule A)
y : A
h :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual f : (a : CharacterModule B) → CharacterModule A) φ : CharacterModule A) : (a : A) → AddCircle 1) y :
      AddCircle (𝕜 := ℚ) 1)
    ((((dual f : (a : CharacterModule B) → CharacterModule A) ψ : CharacterModule A) : (a : A) → AddCircle 1) y :
      AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((φ : (a : B) → AddCircle 1) ((f : (a : A) → B) y) : AddCircle (𝕜 := ℚ) 1)
    ((ψ : (a : B) → AddCircle 1) ((f : (a : A) → B) y) : AddCircle (𝕜 := ℚ) 1)

Tactic:
change (dual f) φ _ = (dual f) ψ _

Premises used: CharacterModule.dual, DFunLike.coe
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
f : A →ₗ[R] B
hf : Function.Surjective.{uA + 1, uB + 1} (α := A) (β := B) (⇑f : (a : A) → B)
φ ψ : CharacterModule B
eq :
  Eq.{uA + 1} (α := CharacterModule A) ((dual f : (a : CharacterModule B) → CharacterModule A) φ : CharacterModule A)
    ((dual f : (a : CharacterModule B) → CharacterModule A) ψ : CharacterModule A)
y : A
h h₁ :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual f : (a : CharacterModule B) → CharacterModule A) ψ : CharacterModule A) : (a : A) → AddCircle 1) y :
      AddCircle (𝕜 := ℚ) 1)
    ((((dual f : (a : CharacterModule B) → CharacterModule A) ψ : CharacterModule A) : (a : A) → AddCircle 1) y :
      AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual f : (a : CharacterModule B) → CharacterModule A) φ : CharacterModule A) : (a : A) → AddCircle 1) y :
      AddCircle (𝕜 := ℚ) 1)
    ((((dual f : (a : CharacterModule B) → CharacterModule A) ψ : CharacterModule A) : (a : A) → AddCircle 1) y :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
rw [eq]
-- Module: Mathlib.Algebra.Module.CharacterModule
Goal:
R : Type uR
inst : CommRing R
A : Type uA
inst_1 : AddCommGroup A
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
f : A →ₗ[R] B
hf : Function.Injective.{uA + 1, uB + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Function.Surjective.{uB + 1, uA + 1} (α := CharacterModule B) (β := CharacterModule A)
    (⇑(dual f) : (a : CharacterModule B) → CharacterModule A)

Tactic:
(Module.Baer.of_divisible _).extension_property_addMonoidHom _ hf

Premises used: Module.Baer.of_divisible, CharacterModule, Function.Surjective, Module.Baer.extension_property_addMonoidHom
-- 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
e : A ≃ₗ[R] B
h :
  ∀ (c : CharacterModule B) (x : B),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
      ((((dual (↑e.symm : B →ₗ[R] A) ∘ₗ dual (↑e : A →ₗ[R] B) : (a : CharacterModule B) → CharacterModule B) c :
              CharacterModule B) :
            (a : B) → AddCircle 1)
          x :
        AddCircle (𝕜 := ℚ) 1)
      ((((LinearMap.id : (a : CharacterModule B) → CharacterModule B) c : CharacterModule B) : (a : B) → AddCircle 1)
          x :
        AddCircle (𝕜 := ℚ) 1)
⊢ dual (↑e.symm : B →ₗ[R] A) ∘ₗ dual (↑e : A →ₗ[R] B) = LinearMap.id

Tactic:
ext c _
-- 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
e : A ≃ₗ[R] B
c : CharacterModule B
x : B
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual (↑e.symm : B →ₗ[R] A) ∘ₗ dual (↑e : A →ₗ[R] B) : (a : CharacterModule B) → CharacterModule B) c :
            CharacterModule B) :
          (a : B) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)
    ((((LinearMap.id : (a : CharacterModule B) → CharacterModule B) c : CharacterModule B) : (a : B) → AddCircle 1) x :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
congr(c $(e.right_inv _))

Premises used: LinearEquiv.right_inv, congrArg, id, 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
e : A ≃ₗ[R] B
c : CharacterModule B
x : B
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual (↑e.symm : B →ₗ[R] A) ∘ₗ dual (↑e : A →ₗ[R] B) : (a : CharacterModule B) → CharacterModule B) c :
            CharacterModule B) :
          (a : B) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)
    ((((LinearMap.id : (a : CharacterModule B) → CharacterModule B) c : CharacterModule B) : (a : B) → AddCircle 1) x :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
exact congr(c $(e.right_inv _))
-- 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
e : A ≃ₗ[R] B
h :
  ∀ (c : CharacterModule A) (x : A),
    Eq (α := AddCircle (𝕜 := ℚ) 1)
      ((((dual (↑e : A →ₗ[R] B) ∘ₗ dual (↑e.symm : B →ₗ[R] A) : (a : CharacterModule A) → CharacterModule A) c :
              CharacterModule A) :
            (a : A) → AddCircle 1)
          x :
        AddCircle (𝕜 := ℚ) 1)
      ((((LinearMap.id : (a : CharacterModule A) → CharacterModule A) c : CharacterModule A) : (a : A) → AddCircle 1)
          x :
        AddCircle (𝕜 := ℚ) 1)
⊢ dual (↑e : A →ₗ[R] B) ∘ₗ dual (↑e.symm : B →ₗ[R] A) = LinearMap.id

Tactic:
ext c _
-- 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
e : A ≃ₗ[R] B
c : CharacterModule A
x : A
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual (↑e : A →ₗ[R] B) ∘ₗ dual (↑e.symm : B →ₗ[R] A) : (a : CharacterModule A) → CharacterModule A) c :
            CharacterModule A) :
          (a : A) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)
    ((((LinearMap.id : (a : CharacterModule A) → CharacterModule A) c : CharacterModule A) : (a : A) → AddCircle 1) x :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
congr(c $(e.left_inv _))

Premises used: congrArg, LinearEquiv.left_inv, id, 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
e : A ≃ₗ[R] B
c : CharacterModule A
x : A
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((((dual (↑e : A →ₗ[R] B) ∘ₗ dual (↑e.symm : B →ₗ[R] A) : (a : CharacterModule A) → CharacterModule A) c :
            CharacterModule A) :
          (a : A) → AddCircle 1)
        x :
      AddCircle (𝕜 := ℚ) 1)
    ((((LinearMap.id : (a : CharacterModule A) → CharacterModule A) c : CharacterModule A) : (a : A) → AddCircle 1) x :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
exact congr(c $(e.left_inv _))
-- 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 c' : LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B)
x : A ⊗[R] B
⊢ 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)

Tactic:
x.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
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)
refine_3 :
  ∀ (x y : A ⊗[R] B),
    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) →
      Eq (α := AddCircle (𝕜 := ℚ) 1)
          (((liftAddHom (c + c').toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1)
              y :
            AddCircle (𝕜 := ℚ) 1)
          ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom ⋯)
                  (liftAddHom c'.toAddMonoidHom ⋯) :
                (a : A ⊗[R] B) → AddCircle 1)
              y :
            AddCircle (𝕜 := ℚ) 1) →
        Eq (α := AddCircle (𝕜 := ℚ) 1)
          (((liftAddHom (c + c').toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1)
              (x + y) :
            AddCircle (𝕜 := ℚ) 1)
          ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom ⋯)
                  (liftAddHom c'.toAddMonoidHom ⋯) :
                (a : A ⊗[R] B) → AddCircle 1)
              (x + 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)

Tactic:
refine x.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
c c' : LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B)
x : A ⊗[R] B
⊢ 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)

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 c' : LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B)
x : A ⊗[R] B
⊢ ∀ (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)

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 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 (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) →
      Eq (α := AddCircle (𝕜 := ℚ) 1)
          (((liftAddHom (c + c').toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1)
              y :
            AddCircle (𝕜 := ℚ) 1)
          ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom ⋯)
                  (liftAddHom c'.toAddMonoidHom ⋯) :
                (a : A ⊗[R] B) → AddCircle 1)
              y :
            AddCircle (𝕜 := ℚ) 1) →
        Eq (α := AddCircle (𝕜 := ℚ) 1)
          (((liftAddHom (c + c').toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1)
              (x + y) :
            AddCircle (𝕜 := ℚ) 1)
          ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom ⋯)
                  (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
r : R
c : LinearMap.{uR, uR, uA, uB} (RingHom.id R) A (CharacterModule B)
x : A ⊗[R] B
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((liftAddHom (r • c).toAddMonoidHom ⋯ : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1) 0)
    ((HSMul.hSMul (α := R) (β := CharacterModule (A ⊗[R] B)) ((RingHom.id R : (a : R) → R) r : R)
          (liftAddHom c.toAddMonoidHom ⋯) :
        (a : A ⊗[R] B) → AddCircle 1)
      0)

Tactic:
simp_rw [map_zero]

Premises used: map_zero