awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
y : L
simp :
  (∃ (a : R), (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) = y) ↔
    ∃ (a : S), HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) = y
⊢ Membership.mem (γ := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
        (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (R ∙ x)) ⋯)
      y ↔
    Membership.mem (γ := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      (spanSingleton S⁰ ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x) :
        FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      y

Tactic:
simp only [← FractionalIdeal.mem_coe, coe_mk, mem_map_equiv, coe_spanSingleton,
    Submodule.mem_span_singleton, (semilinearEquivOfRingEquiv K L f).eq_symm_apply]

Premises used: LinearEquiv.eq_symm_apply, Submodule.mem_span_singleton, FractionalIdeal.coe_mk, FractionalIdeal.mem_coe, FractionalIdeal.coe_spanSingleton, IsFractionRing.semilinearEquivOfRingEquiv, Submodule.mem_map_equiv
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
y : L
mp :
  (∃ (a : R), (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) = y) →
    ∃ (a : S), HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) = y
mpr :
  (∃ (a : S), HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) = y) →
    ∃ (a : R), (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) = y
⊢ (∃ (a : R), (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) = y) ↔
    ∃ (a : S), HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) = y

Tactic:
constructor
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
r : R
h :
  HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) =
    (semilinearEquivOfRingEquiv K L f : (a : K) → L) (r • x)
⊢ ∃ (a : S),
    HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) =
      (semilinearEquivOfRingEquiv K L f : (a : K) → L) (r • x)

Tactic:
use f r

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
r : R
⊢ HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) =
    (semilinearEquivOfRingEquiv K L f : (a : K) → L) (r • x)

Tactic:
.symm (map_smulₛₗ _ r x)

Premises used: MulActionSemiHomClass.map_smulₛₗ, Eq.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
r : R
⊢ HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
      ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) =
    (semilinearEquivOfRingEquiv K L f : (a : K) → L) (r • x)

Tactic:
exact .symm (map_smulₛₗ _ r x)
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
s : S
h :
  (semilinearEquivOfRingEquiv K L f : (a : K) → L)
      (HSMul.hSMul.{u_5, u_7, u_7} (α := R) ((f.symm : (a : S) → R) s : R) x) =
    HSMul.hSMul (β := L) s ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L)
⊢ ∃ (a : R),
    (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) =
      HSMul.hSMul (β := L) s ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L)

Tactic:
use f.symm s

Premises used: DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
s : S
⊢ (semilinearEquivOfRingEquiv K L f : (a : K) → L)
      (HSMul.hSMul.{u_5, u_7, u_7} (α := R) ((f.symm : (a : S) → R) s : R) x) =
    HSMul.hSMul (β := L) s ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L)

Tactic:
simp only [Algebra.smul_def, semilinearEquivOfRingEquiv_apply, map_mul, map_eq, RingHom.coe_coe,
      IsFractionRing.ringEquivOfRingEquiv_apply, RingEquiv.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply, IsFractionRing.ringEquivOfRingEquiv_apply, RingHom.coe_coe, IsLocalization.map_eq, IsFractionRing.semilinearEquivOfRingEquiv_apply, map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
⊢ Eq (α := RingEquiv.{u_8, u_7} (FractionalIdeal.{u_6, u_8} (R := S) S⁰ L) (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K))
    (RingEquiv.symm (ringEquivOfRingEquiv K L f)) (ringEquivOfRingEquiv L K f.symm)

Tactic:
(RingEquiv.coe_nonUnitalRingHom_inj_iff (ringEquivOfRingEquiv K L f).symm
          (ringEquivOfRingEquiv L K f.symm)).mpr rfl

Premises used: Iff.mpr, RingEquiv.coe_nonUnitalRingHom_inj_iff, FractionalIdeal.ringEquivOfRingEquiv, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
⊢ Eq (α := RingEquiv.{u_8, u_7} (FractionalIdeal.{u_6, u_8} (R := S) S⁰ L) (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K))
    (RingEquiv.symm (ringEquivOfRingEquiv K L f)) (ringEquivOfRingEquiv L K f.symm)

Tactic:
exact (RingEquiv.coe_nonUnitalRingHom_inj_iff (ringEquivOfRingEquiv K L f).symm
          (ringEquivOfRingEquiv L K f.symm)).mpr rfl

Premises used: Iff.mpr, RingEquiv.coe_nonUnitalRingHom_inj_iff, FractionalIdeal.ringEquivOfRingEquiv, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
⊢ Function.Injective.{u + 1, u + 1} (α := α) of

Tactic:
FreeAbelianGroup.of_injective.comp fun _ _ =>
    (Multiset.coe_eq_coe.trans List.singleton_perm_singleton).mp

Premises used: FreeCommRing, FreeCommRing.of, List.singleton_perm_singleton, Multiset.coe_eq_coe, Function.Injective.comp, FreeAbelianGroup.of, FreeAbelianGroup.of_injective, Iff.mp, Iff.trans
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : α
⊢ of x ≠ 0

Tactic:
FreeAbelianGroup.of_ne_zero _

Premises used: FreeCommRing, FreeAbelianGroup.of_ne_zero, FreeCommRing.of
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : α
⊢ 0 ≠ of x

Tactic:
FreeAbelianGroup.zero_ne_of _

Premises used: FreeCommRing, FreeAbelianGroup.zero_ne_of, FreeCommRing.of
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : α
⊢ of x ≠ 1

Tactic:
FreeAbelianGroup.of_injective.ne <| Multiset.singleton_ne_zero _

Premises used: FreeCommRing, FreeCommRing.of, Function.Injective.ne, FreeAbelianGroup.of, FreeAbelianGroup.of_injective, Multiset.singleton_ne_zero
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : α
⊢ 1 ≠ of x

Tactic:
FreeAbelianGroup.of_injective.ne <| Multiset.zero_ne_singleton _

Premises used: FreeCommRing, Multiset.zero_ne_singleton, FreeCommRing.of, Function.Injective.ne, FreeAbelianGroup.of, FreeAbelianGroup.of_injective
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
a : α
m : Multiset α
rw :
  FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) ({a} + m)) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
rw₁ :
  FreeAbelianGroup.of
      (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α))) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
rw₂ :
  FreeAbelianGroup.of
      (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α))) =
    HMul.hMul (α := FreeAbelianGroup (Multiplicative (Multiset α))) (β :=
      FreeAbelianGroup (Multiplicative (Multiset α)))
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a}) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
rw₃ rw₄ :
  FreeAbelianGroup.of
      (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α))) =
    FreeAbelianGroup.of
      (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α)))
⊢ FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) (a ::ₘ m)) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))

Tactic:
rw [← Multiset.singleton_add, ofAdd_add,
    of, FreeAbelianGroup.of_mul_of]

Premises used: Multiset.singleton_add, FreeCommRing.of, FreeAbelianGroup.of_mul_of, ofAdd_add
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
motive : FreeCommRing α → Prop
z : FreeCommRing α
neg_one : motive (-1)
of : ∀ (b : α), motive (FreeCommRing.of b)
add : ∀ (x y : FreeCommRing α), motive x → motive y → motive (x + y)
mul : ∀ (x y : FreeCommRing α), motive x → motive y → motive (x * y)
⊢ motive z

Tactic:
have neg : ∀ x, motive x → motive (-x) := fun x ih => neg_one_mul x ▸ mul _ _ neg_one ih
  have one : motive 1 := neg_neg (1 : FreeCommRing α) ▸ neg _ neg_one
  FreeAbelianGroup.induction_on z (neg_add_cancel (1 : FreeCommRing α) ▸ add _ _ neg_one one)
    (fun m => Multiset.induction_on m one fun a _ ih => mul (FreeCommRing.of a) _ (of a) ih)
    (fun _ ih => neg _ ih) add

Premises used: FreeAbelianGroup.induction_on, neg_one_mul, Eq.rec, neg_neg, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f_1 f : α → R
x y : Multiplicative (Multiset α)
rw :
  (Multiset.map f ((Multiplicative.toAdd : (a : Multiplicative (Multiset α)) → Multiset α) (x * y))).prod =
    (Multiset.map f (x + y)).prod
⊢ (Multiset.map f ((Multiplicative.toAdd : (a : Multiplicative (Multiset α)) → Multiset α) (x * y))).prod =
    (Multiset.map f x + Multiset.map f y).prod

Tactic:
rw [← Multiset.map_add]

Premises used: Multiset.map_add
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f_1 f : α → R
x y : Multiplicative (Multiset α)
⊢ (Multiset.map f ((Multiplicative.toAdd : (a : Multiplicative (Multiset α)) → Multiset α) (x * y))).prod =
    (Multiset.map f (x + y)).prod

Tactic:
rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f_1 f : α → R
x : α
⊢ (Multiset.map f {x}).prod = f x

Tactic:
simp
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f : α → R
F : MonoidHom.{u, v} (Multiplicative (Multiset α)) R
x : Multiplicative (Multiset α)
F' : AddMonoidHom.{u, v} (Multiset α) (Additive R) :=
  (MonoidHom.toAdditiveRight : (a : Multiplicative (Multiset α) →* R) → Multiset α →+ Additive R) F
x' : Multiset α := (Multiplicative.toAdd : (a : Multiplicative (Multiset α)) → Multiset α) x
rw :
  Eq.{v + 1} (α := Additive R)
    ((F' : (a : Multiset α) → Additive R) (Multiset.sum (Multiset.map (fun (x : α) ↦ {x}) x')) : Additive R)
    ((F' : (a : Multiset α) → Additive R) x' : Additive R)
⊢ Eq.{v + 1} (α := Additive R)
    (Multiset.sum (Multiset.map (fun (a : α) ↦ (F' : (a : Multiset α) → Additive R) {a}) x') : Additive R)
    ((F' : (a : Multiset α) → Additive R) x' : Additive R)

Tactic:
rw [← Function.comp_def (fun x => F' x) (fun x => {x}), ← Multiset.map_map,
        ← AddMonoidHom.map_multiset_sum]

Premises used: Function.comp_def, Multiset.map_map, AddMonoidHom.map_multiset_sum, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f : α → R
F : MonoidHom.{u, v} (Multiplicative (Multiset α)) R
x : Multiplicative (Multiset α)
F' : AddMonoidHom.{u, v} (Multiset α) (Additive R) :=
  (MonoidHom.toAdditiveRight : (a : Multiplicative (Multiset α) →* R) → Multiset α →+ Additive R) F
x' : Multiset α := (Multiplicative.toAdd : (a : Multiplicative (Multiset α)) → Multiset α) x
⊢ Eq.{v + 1} (α := Additive R)
    ((F' : (a : Multiset α) → Additive R) (Multiset.sum (Multiset.map (fun (x : α) ↦ {x}) x')) : Additive R)
    ((F' : (a : Multiset α) → Additive R) x' : Additive R)

Tactic:
DFunLike.congr_arg F (Multiset.sum_map_singleton x')

Premises used: Additive, Multiset.sum_map_singleton, DFunLike.congr_arg
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f : α → R
F : MonoidHom.{u, v} (Multiplicative (Multiset α)) R
x : Multiplicative (Multiset α)
F' : AddMonoidHom.{u, v} (Multiset α) (Additive R) :=
  (MonoidHom.toAdditiveRight : (a : Multiplicative (Multiset α) →* R) → Multiset α →+ Additive R) F
x' : Multiset α := (Multiplicative.toAdd : (a : Multiplicative (Multiset α)) → Multiset α) x
⊢ Eq.{v + 1} (α := Additive R)
    ((F' : (a : Multiset α) → Additive R) (Multiset.sum (Multiset.map (fun (x : α) ↦ {x}) x')) : Additive R)
    ((F' : (a : Multiset α) → Additive R) x' : Additive R)

Tactic:
exact DFunLike.congr_arg F (Multiset.sum_map_singleton x')

Premises used: Multiset.sum_map_singleton, DFunLike.congr_arg
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f : α → R
x : α
⊢ (((lift : (a : α → R) → FreeCommRing α →+* R) f : RingHom.{u, v} (FreeCommRing α) R) : (a : FreeCommRing α) → R)
      (of x) =
    f x

Tactic:
(FreeAbelianGroup.lift_apply_of _ _).trans <| mul_one _

Premises used: FreeCommRing.of, mul_one, FreeAbelianGroup.lift_apply_of, Eq.trans
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x : FreeCommRing α
rw :
  Eq.{v + 1} (α := R)
    (-(((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          1 :
      R)
    ((f : (a : FreeCommRing α) → R) (-1) : R)
rw₁ : Eq.{v + 1} (α := R) (-1 : R) ((f : (a : FreeCommRing α) → R) (-1) : R)
rw₂ : Eq.{v + 1} (α := R) (-1 : R) (-(f : (a : FreeCommRing α) → R) 1 : R)
rw₃ rw₄ : Eq.{v + 1} (α := R) (-1) (-1)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (-1) :
      R)
    ((f : (a : FreeCommRing α) → R) (-1) : R)

Tactic:
rw [map_neg, map_one, f.map_neg, f.map_one]

Premises used: RingHom.map_neg, RingHom.map_one, map_neg, map_one
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x_1 x y : FreeCommRing α
ihx :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((f : (a : FreeCommRing α) → R) x : R)
ihy :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R)
    ((f : (a : FreeCommRing α) → R) y : R)
rw :
  HAdd.hAdd (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    (f : (a : FreeCommRing α) → R) (x + y)
rw₁ :
  HAdd.hAdd (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
rw₂ :
  HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
rw₃ rw₄ :
  HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R) =
    HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (x + y) :
      R)
    ((f : (a : FreeCommRing α) → R) (x + y) : R)

Tactic:
rw [map_add, f.map_add, ihx, ihy]

Premises used: map_add, RingHom.map_add
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x_1 x y : FreeCommRing α
ihx :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((f : (a : FreeCommRing α) → R) x : R)
ihy :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R)
    ((f : (a : FreeCommRing α) → R) y : R)
rw :
  HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    (f : (a : FreeCommRing α) → R) (x * y)
rw₁ :
  HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
rw₂ :
  HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
rw₃ rw₄ :
  HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (x * y) :
      R)
    ((f : (a : FreeCommRing α) → R) (x * y) : R)

Tactic:
rw [map_mul, f.map_mul, ihx, ihy]

Premises used: map_mul, RingHom.map_mul
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
R : Type v
inst : CommRing R
f g : RingHom.{u, v} (FreeCommRing α) R
h :
  ∀ (x : α), Eq.{v + 1} (α := R) ((f : (a : FreeCommRing α) → R) (of x) : R) ((g : (a : FreeCommRing α) → R) (of x) : R)
⊢ f = g

Tactic:
lift.symm.injective (funext h)

Premises used: funext, Equiv.injective, Equiv.symm, FreeCommRing.lift
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
β : Type v
f : α → β
x : α
⊢ (map f : (a : FreeCommRing α) → FreeCommRing β) (of x) = of (f x)

Tactic:
lift_of _ _

Premises used: FreeCommRing.lift_of, FreeCommRing.of, FreeAbelianGroup.of
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeCommRing α
s t : Set α
hs : x.IsSupported s
hst : s ⊆ t
⊢ x.IsSupported t

Tactic:
Subring.closure_mono (Set.monotone_image hst) hs

Premises used: FreeCommRing.IsSupported, Subring.closure_mono, Set.monotone_image