awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
f : α → R
g : α → M
x : α
hfg : x ∈ support (f • g)
hf : f x = 0
rw : f x • g x = 0
⊢ (f • g) x = 0
have rw₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := R) 0 (g x) = 0
Tactic: rw [Pi.smul_apply', hf, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
f : α → R
g : α → M
x : α
hfg : x ∈ support (f • g)
hf : f x = 0
rw : f x • g x = 0
rw₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := R) 0 (g x) = 0
⊢ (f • g) x = 0
have rw₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [Pi.smul_apply', hf, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
f : α → R
g : α → M
x : α
hbf : x ∈ support (f • g)
hf : g x = 0
⊢ (f • g) x = 0
have rw : f x • g x = 0
Tactic: rw [Pi.smul_apply', hf, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
f : α → R
g : α → M
x : α
hbf : x ∈ support (f • g)
hf : g x = 0
rw : f x • g x = 0
⊢ (f • g) x = 0
have rw₁ : HSMul.hSMul (β := M) (f x) 0 = 0
Tactic: rw [Pi.smul_apply', hf, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
f : α → R
g : α → M
x : α
hbf : x ∈ support (f • g)
hf : g x = 0
rw : f x • g x = 0
rw₁ : HSMul.hSMul (β := M) (f x) 0 = 0
⊢ (f • g) x = 0
have rw₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [Pi.smul_apply', hf, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
⊢ s.indicator (fun (a : α) ↦ r a • f a) a = r a • s.indicator f a
have dsimp : (if a ∈ s then r a • f a else 0) = r a • if a ∈ s then f a else 0
Tactic: dsimp only [indicator]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
⊢ (if a ∈ s then r a • f a else 0) = r a • if a ∈ s then f a else 0
have pos : a ∈ s → r a • f a = r a • f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
pos : a ∈ s → r a • f a = r a • f a
⊢ (if a ∈ s then r a • f a else 0) = r a • if a ∈ s then f a else 0
have neg : ¬a ∈ s → 0 = HSMul.hSMul (β := M) (r a) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
⊢ s.indicator (fun (a : α) ↦ r a • f a) a = s.indicator r a • f a
have dsimp : (if a ∈ s then r a • f a else 0) = (if a ∈ s then r a else 0) • f a
Tactic: dsimp only [indicator]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
⊢ (if a ∈ s then r a • f a else 0) = (if a ∈ s then r a else 0) • f a
have pos : a ∈ s → r a • f a = r a • f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
pos : a ∈ s → r a • f a = r a • f a
⊢ (if a ∈ s then r a • f a else 0) = (if a ∈ s then r a else 0) • f a
have neg : ¬a ∈ s → 0 = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 0 (f a)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
inst : MulZeroOneClass R
s : Set α
r : R
a : α
⊢ HSMul.hSMul (β := R) r (s.indicator 1 a) = s.indicator (fun (x : α) ↦ r) a
have simp_rw : Eq.{u_2 + 1} (α := R) (s.indicator (fun (x : α) ↦ HSMul.hSMul (β := R) r (1 x)) a) (s.indicator (fun (x : α) ↦ r) a)
Tactic: simp_rw [← indicator_const_smul_apply, Pi.one_apply, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
inst : MulZeroOneClass R
s : Set α
r : R
a : α
simp_rw :
  Eq.{u_2 + 1} (α := R) (s.indicator (fun (x : α) ↦ HSMul.hSMul (β := R) r (1 x)) a) (s.indicator (fun (x : α) ↦ r) a)
⊢ HSMul.hSMul (β := R) r (s.indicator 1 a) = s.indicator (fun (x : α) ↦ r) a
have simp_rw₁ : Eq.{u_2 + 1} (α := R) (s.indicator (fun (x : α) ↦ HSMul.hSMul (β := R) r 1) a) (s.indicator (fun (x : α) ↦ r) a)
Tactic: simp_rw [← indicator_const_smul_apply, Pi.one_apply, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
inst : MulZeroOneClass R
s : Set α
r : R
a : α
simp_rw :
  Eq.{u_2 + 1} (α := R) (s.indicator (fun (x : α) ↦ HSMul.hSMul (β := R) r (1 x)) a) (s.indicator (fun (x : α) ↦ r) a)
simp_rw₁ :
  Eq.{u_2 + 1} (α := R) (s.indicator (fun (x : α) ↦ HSMul.hSMul (β := R) r 1) a) (s.indicator (fun (x : α) ↦ r) a)
⊢ HSMul.hSMul (β := R) r (s.indicator 1 a) = s.indicator (fun (x : α) ↦ r) a
have simp_rw₂ : Eq.{u_2 + 1} (α := R) (s.indicator (fun (x : α) ↦ r * 1) a) (s.indicator (fun (x : α) ↦ r) a)
Tactic: simp_rw [← indicator_const_smul_apply, Pi.one_apply, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.BigOperators (goal)
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Multiset R
t : Multiset M
⊢ s.sum • t.sum = sum (map (fun (p : R × M) ↦ p.1 • p.2) (s ×ˢ t))
have empty : HSMul.hSMul.{u_5, u_6, u_6} (α := R) (sum 0) t.sum =
  sum (map (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Multiset R) 0 t))
Tactic: induction s using Multiset.induction with
  | empty => simp
  | cons a s ih => simp [add_smul, ih, ← Multiset.smul_sum]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Module.BigOperators (goal)
Goal:
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Multiset R
t : Multiset M
empty :
  HSMul.hSMul.{u_5, u_6, u_6} (α := R) (sum 0) t.sum =
    sum (map (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Multiset R) 0 t))
⊢ s.sum • t.sum = sum (map (fun (p : R × M) ↦ p.1 • p.2) (s ×ˢ t))
have cons : ∀ (a : R) (s : Multiset R) (ih : s.sum • t.sum = sum (map (fun (p : R × M) ↦ p.1 • p.2) (s ×ˢ t))),
  (a ::ₘ s).sum • t.sum = sum (map (fun (p : R × M) ↦ p.1 • p.2) ((a ::ₘ s) ×ˢ t))
Tactic: induction s using Multiset.induction with
  | empty => simp
  | cons a s ih => simp [add_smul, ih, ← Multiset.smul_sum]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Module.BigOperators (goal)
Goal:
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset α
t : Finset β
f : α → R
g : β → M
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := R) (β := M) (∑ i ∈ s, f i) (∑ j ∈ t, g j) = ∑ i ∈ s, ∑ j ∈ t, f i • g j
have simp_rw : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, HSMul.hSMul (β := M) (f i) (∑ j ∈ t, g j)) (∑ i ∈ s, ∑ j ∈ t, f i • g j)
Tactic: simp_rw [sum_smul, ← smul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Module.BigOperators (goal)
Goal:
α : Type u_3
R : Type u_5
inst : NonAssocSemiring R
s : Finset α
⊢ Eq.{u_5 + 1} (α := R) (↑(#s) : R) (∑ x ∈ s, 1)
have rw : (↑(#s) : R) = HSMul.hSMul (β := R) (#s) 1
Tactic: rw [Finset.sum_const, Nat.smul_one_eq_cast]
-- Lean 4 proof step from Mathlib.Algebra.Module.BigOperators (goal)
Goal:
α : Type u_3
R : Type u_5
inst : NonAssocSemiring R
s : Finset α
rw : (↑(#s) : R) = HSMul.hSMul (β := R) (#s) 1
⊢ Eq.{u_5 + 1} (α := R) (↑(#s) : R) (∑ x ∈ s, 1)
have rw₁ : Eq.{u_5 + 1} (α := R) (↑(#s) : R) (↑(#s) : R)
Tactic: rw [Finset.sum_const, Nat.smul_one_eq_cast]
-- Lean 4 proof step from Mathlib.Algebra.Module.BigOperators (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ g ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s, f (g i) =
    HSMul.hSMul (β := α) (#s ^ (card ι - 1)) (∑ b ∈ s, f b)
have rw : ∑ b ∈ image (fun (g : (a : ι) → κ) ↦ g i) (piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s),
    Finset.card (α := (a : ι) → κ) ({a ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s | a i = b}) • f b =
  HSMul.hSMul (β := α) (#s ^ (card ι - 1)) (∑ b ∈ s, f b)
Tactic: rw [Finset.sum_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.BigOperators (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ g ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s, f (g i) =
    HSMul.hSMul (β := α) (#s ^ (card ι - 1)) (∑ b ∈ s, f b)
have rw : ∑ b ∈ image (fun (g : (a : ι) → κ) ↦ g i) (piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s),
    Finset.card (α := (a : ι) → κ) ({a ∈ piFinset (δ := fun (x : ι) ↦ κ) fun (x : ι) ↦ s | a i = b}) • f b =
  HSMul.hSMul (β := α) (#s ^ (card ι - 1)) (∑ b ∈ s, f b)
Tactic: classical
  rw [Finset.sum_comp]
  simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum,
    Finset.sum_ite_mem, inter_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : AddCommMonoid α
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∑ i : ι, HSMul.hSMul.{u_7, u_3, u_3} (α := R) (Pi.single (M := fun (x : ι) ↦ R) i₀ r i : R) (f i) = r • f i₀
have h₀ : ∀ (b : ι),
  Membership.mem (γ := Finset ι) univ b →
    b ≠ i₀ → HSMul.hSMul.{u_7, u_3, u_3} (α := R) (Pi.single (M := fun (x : ι) ↦ R) i₀ r b : R) (f b) = 0
Tactic: rw [Finset.sum_eq_single i₀, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.Module.BigOperators (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : AddCommMonoid α
R : Type u_7
inst_3 : Semiring R
inst_4 : Module R α
f : ι → α
r : R
i₀ : ι
h₀ :
  ∀ (b : ι),
    Membership.mem (γ := Finset ι) univ b →
      b ≠ i₀ → HSMul.hSMul.{u_7, u_3, u_3} (α := R) (Pi.single (M := fun (x : ι) ↦ R) i₀ r b : R) (f b) = 0
⊢ ∑ i : ι, HSMul.hSMul.{u_7, u_3, u_3} (α := R) (Pi.single (M := fun (x : ι) ↦ R) i₀ r i : R) (f i) = r • f i₀
have h₁ : i₀ ∉ univ → HSMul.hSMul.{u_7, u_3, u_3} (α := R) (Pi.single (M := fun (x : ι) ↦ R) i₀ r i₀ : R) (f i₀) = 0
Tactic: rw [Finset.sum_eq_single i₀, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.Module.Bimodule (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m ∈ p
have suffices : a • m = HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] 1) m
Tactic: suffices a • m = a ⊗ₜ[R] (1 : B) • m by exact this.symm ▸ p.smul_mem _ hm
-- Lean 4 proof step from Mathlib.Algebra.Module.Bimodule (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m ∈ p
have suffices : b • m = HSMul.hSMul (α := A ⊗[R] B) (1 ⊗ₜ[R] b) m
Tactic: suffices b • m = (1 : A) ⊗ₜ[R] b • m by exact this.symm ▸ p.smul_mem _ hm
-- Lean 4 proof step from Mathlib.Algebra.Module.Card (goal)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : Ring R
inst_2 : IsDomain R
inst_3 : Module R E
inst_4 : Nontrivial E
inst_5 : Module.IsTorsionFree R E
⊢ lift.{v, u} #R ≤ lift.{u, v} #E
have obtain : ∀ (x : E) (hx : x ≠ 0), lift.{v, u} #R ≤ lift.{u, v} #E
Tactic: obtain ⟨x, hx⟩ : ∃ (x : E), x ≠ 0 := exists_ne 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Card (hypothesis)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : Ring R
inst_2 : IsDomain R
inst_3 : Module R E
inst_4 : Nontrivial E
inst_5 : Module.IsTorsionFree R E
x : E
hx : x ≠ 0
⊢ lift.{v, u} #R ≤ lift.{u, v} #E
have this : Injective.{u + 1, v + 1} (β := E) fun (k : R) ↦ k • x
Tactic: have : Injective (fun k ↦ k • x) := smul_left_injective R hx
-- 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
f : A →ₗ[R] B
r : R
c : CharacterModule B
⊢ AddMonoidHom.comp (r • c) f.toAddMonoidHom =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (AddMonoidHom.comp c f.toAddMonoidHom)
have 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)
Tactic: ext 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
B : Type uB
inst_2 : AddCommGroup B
inst_3 : Module R A
inst_4 : Module R B
⊢ Eq (α := LinearMap.{uR, uR, uB, uA} (RingHom.id R) (CharacterModule B) (CharacterModule A)) (dual 0) 0
have 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)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
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
⊢ dual (g ∘ₗ f) = dual f ∘ₗ dual g
have 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)
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
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)
⊢ φ = ψ
have h : ∀ (x : B),
  Eq (α := AddCircle (𝕜 := ℚ) 1) ((φ : (a : B) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
    ((ψ : (a : B) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
Tactic: ext 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
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
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1) ((φ : (a : B) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
    ((ψ : (a : B) → AddCircle 1) x : AddCircle (𝕜 := ℚ) 1)
have 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)
Tactic: obtain ⟨y, rfl⟩ := hf x
Cleared hypotheses: 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
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
⊢ 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)
have 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)
Tactic: change (dual f) φ _ = (dual f) ψ _
-- Lean 4 proof step from Mathlib.Algebra.Module.CharacterModule (goal)
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
⊢ 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)
have 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)
Tactic: rw [eq]
-- 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
e : A ≃ₗ[R] B
⊢ dual (↑e.symm : B →ₗ[R] A) ∘ₗ dual (↑e : A →ₗ[R] B) = LinearMap.id
have 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)
Tactic: ext 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'
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
⊢ dual (↑e : A →ₗ[R] B) ∘ₗ dual (↑e.symm : B →ₗ[R] A) = LinearMap.id
have 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)
Tactic: ext 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'
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)
have refine_1 : Eq (α := AddCircle (𝕜 := ℚ) 1)
  (((liftAddHom (c + c').toAddMonoidHom sorry : A ⊗[R] B →+ AddCircle (𝕜 := ℚ) 1) : (a : A ⊗[R] B) → AddCircle 1) 0)
  ((HAdd.hAdd (α := CharacterModule (A ⊗[R] B)) (liftAddHom c.toAddMonoidHom sorry) (liftAddHom c'.toAddMonoidHom sorry) :
      (a : A ⊗[R] B) → AddCircle 1)
    0)
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 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)
⊢ 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_2 : ∀ (x : A) (y : B),
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((liftAddHom (c + c').toAddMonoidHom sorry : 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 sorry) (liftAddHom c'.toAddMonoidHom sorry) :
          (a : A ⊗[R] B) → AddCircle 1)
        (x ⊗ₜ[R] y) :
      AddCircle (𝕜 := ℚ) 1)
Tactic: refine x.induction_on ?_ ?_ ?_