awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : Free R S
⊢ Free R R[X]

Tactic:
.of_equiv (Polynomial.toFinsuppIsoLinear _).symm

Premises used: LinearEquiv.symm, Module.Free.of_equiv, Polynomial.toFinsuppIsoLinear
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
U : Type u_2
V : Type u_3
inst_1 : AddCommMonoid U
inst_2 : AddCommMonoid V
inst_3 : Module R U
inst_4 : Module R V
e : V ≃ₗ[R] V
f : V →ₗ[R] V
x y : V
hx : Membership.mem (γ := Set V) {x : V | (f : (a : V) → V) x = x} x
hy : Membership.mem (γ := Set V) {x : V | (f : (a : V) → V) x = x} y
⊢ Membership.mem (γ := Set V) {x : V | (f : (a : V) → V) x = x} (x + y)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
U : Type u_2
V : Type u_3
inst_1 : AddCommMonoid U
inst_2 : AddCommMonoid V
inst_3 : Module R U
inst_4 : Module R V
e : V ≃ₗ[R] V
f : V →ₗ[R] V
⊢ Membership.mem (γ := Set V) {x : V | (f : (a : V) → V) x = x} 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
U : Type u_2
V : Type u_3
inst_1 : AddCommMonoid U
inst_2 : AddCommMonoid V
inst_3 : Module R U
inst_4 : Module R V
e : V ≃ₗ[R] V
f : V →ₗ[R] V
r : R
x : V
hx : Membership.mem (γ := Set V) {x : V | (f : (a : V) → V) x = x} x
⊢ Membership.mem (γ := Set V) {x : V | (f : (a : V) → V) x = x} (r • x)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : V →ₗ[R] V
v : V
⊢ v ∈ f.fixedSubmodule ↔ (f : (a : V) → V) v = v

Tactic:
simp [fixedSubmodule]

Premises used: LinearMap.fixedSubmodule
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
inst : Ring R
V : Type u_5
inst_1 : AddCommGroup V
inst_2 : Module R V
f : V →ₗ[R] V
h : ∀ (x : V), x ∈ f.fixedSubmodule ↔ x ∈ (f - id).ker
⊢ f.fixedSubmodule = (f - id).ker

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
inst : Ring R
V : Type u_5
inst_1 : AddCommGroup V
inst_2 : Module R V
f : V →ₗ[R] V
x : V
⊢ x ∈ f.fixedSubmodule ↔ x ∈ (f - id).ker

Tactic:
simp [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : V →ₗ[R] V
⊢ f.fixedSubmodule = ⊤ ↔ f = id

Tactic:
simp [LinearMap.ext_iff, Submodule.ext_iff]

Premises used: Submodule.ext_iff, LinearMap.ext_iff
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
f g : V →ₗ[R] V
x : V
⊢ x ∈ f.fixedSubmodule ⊓ g.fixedSubmodule → x ∈ (f ∘ₗ g).fixedSubmodule

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
f g : V →ₗ[R] V
x : V
⊢ x ∈ (f ∘ₗ g).fixedSubmodule ⊓ g.fixedSubmodule → x ∈ f.fixedSubmodule

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : V ≃ₗ[R] V
⊢ (↑f : V →ₗ[R] V).fixedSubmodule = ⊤ ↔ f = refl R V

Tactic:
simp [LinearEquiv.ext_iff, Submodule.ext_iff]

Premises used: Submodule.ext_iff, LinearEquiv.ext_iff
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
a : map (DistribSMul.toLinearMap R V e) W ≤ W
a₁ : W ≤ map (DistribSMul.toLinearMap R V e) W
⊢ map (DistribSMul.toLinearMap R V e) W = W

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
this : (e : (a : V) → V) x = x
⊢ Membership.mem (α := V) W ((DistribSMul.toLinearMap R V e : (a : V) → V) x : V)

Tactic:
simpa [this, coe_coe]

Premises used: LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
a : (e : (a : V) → V) x = x
⊢ Membership.mem (α := V) W ((DistribSMul.toLinearMap R V e : (a : V) → V) x : V)

Tactic:
suffices e x = x by simpa [this, coe_coe]
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
a : x ∈ (↑e : V →ₗ[R] V).fixedSubmodule
⊢ (e : (a : V) → V) x = x

Tactic:
rw [← coe_toLinearMap, ← mem_fixedSubmodule_iff]

Premises used: LinearEquiv.coe_toLinearMap, LinearMap.mem_fixedSubmodule_iff
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
⊢ x ∈ (↑e : V →ₗ[R] V).fixedSubmodule

Tactic:
hW hx
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
⊢ x ∈ (↑e : V →ₗ[R] V).fixedSubmodule

Tactic:
exact hW hx
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
⊢ x ∈ map (DistribSMul.toLinearMap R V e) W

Tactic:
⟨x, hx, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
a : (DistribSMul.toLinearMap R V e : (a : V) → V) x = x
⊢ x ∈ map (DistribSMul.toLinearMap R V e) W

Tactic:
refine ⟨x, hx, ?_⟩
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
a : (e : (a : V) → V) x = x
⊢ (DistribSMul.toLinearMap R V e : (a : V) → V) x = x

Tactic:
simp only [DistribSMul.toLinearMap_apply, LinearEquiv.smul_def]

Premises used: DistribSMul.toLinearMap_apply, LinearEquiv.smul_def
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
⊢ Membership.mem (γ := Subgroup (V ≃ₗ[R] V)) (stabilizer (V ≃ₗ[R] V) (↑e : V →ₗ[R] V).fixedSubmodule) e

Tactic:
mem_stabilizer_submodule_of_le_fixedSubmodule (le_refl _)

Premises used: le_refl, LinearEquiv.mem_stabilizer_submodule_of_le_fixedSubmodule
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
he : Membership.mem (γ := Subgroup (V ≃ₗ[R] V)) (fixingSubgroup (V ≃ₗ[R] V) W.carrier) e
h : ∀ (v : V), v ∈ map (↑e : V →ₗ[R] V) W ↔ v ∈ W
⊢ map (↑e : V →ₗ[R] V) W = W

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
he : Membership.mem (γ := Subgroup (V ≃ₗ[R] V)) (fixingSubgroup (V ≃ₗ[R] V) W.carrier) e
v : V
⊢ ∀ y ∈ W, (e : (a : V) → V) y = y

Tactic:
simp only [mem_fixingSubgroup_iff, carrier_eq_coe, SetLike.mem_coe, LinearEquiv.smul_def] at he

Premises used: SetLike.mem_coe, LinearEquiv.smul_def, mem_fixingSubgroup_iff, Submodule.carrier_eq_coe
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, (e : (a : V) → V) y = y
⊢ v ∈ map (↑e : V →ₗ[R] V) W ↔ v ∈ W

Tactic:
⟨fun ⟨w, hv, hv'⟩ ↦ ?_, fun hv ↦ ?_⟩

Premises used: Membership.mem, _private.0.LinearEquiv.map_eq_of_mem_fixingSubgroup.match_2, Iff.intro
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, (e : (a : V) → V) y = y
h : v ∈ map (↑e : V →ₗ[R] V) W → ∀ (w : V) (hv : w ∈ (↑W : Set V)) (hv' : ((↑e : V →ₗ[R] V) : (a : V) → V) w = v), v ∈ W
h₁ : ∀ (hv : v ∈ W), v ∈ map (↑e : V →ₗ[R] V) W
⊢ v ∈ map (↑e : V →ₗ[R] V) W ↔ v ∈ W

Tactic:
refine ⟨fun ⟨w, hv, hv'⟩ ↦ ?_, fun hv ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, (e : (a : V) → V) y = y
h : v ∈ map (↑e : V →ₗ[R] V) W
w : V
hv : w ∈ (↑W : Set V)
hv' : ((↑e : V →ₗ[R] V) : (a : V) → V) w = v
⊢ w ∈ W

Tactic:
simp only [SetLike.mem_coe, coe_coe] at hv hv'

Premises used: SetLike.mem_coe, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, (e : (a : V) → V) y = y
h_1 : v ∈ map (↑e : V →ₗ[R] V) W
w : V
hv' : (e : (a : V) → V) w = v
hv : w ∈ W
h : Membership.mem (α := V) W ((e : (a : V) → V) w : V)
h₁ h₂ h₃ h₄ : w ∈ W
⊢ v ∈ W

Tactic:
rwa [← hv', he w hv]
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, (e : (a : V) → V) y = y
hv : v ∈ W
⊢ v ∈ map (↑e : V →ₗ[R] V) W

Tactic:
⟨v, hv, he v hv⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, (e : (a : V) → V) y = y
hv : v ∈ W
⊢ v ∈ map (↑e : V →ₗ[R] V) W

Tactic:
refine ⟨v, hv, he v hv⟩
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R_1 : Type u_1
inst : Semiring R_1
U : Type u_2
V_1 : Type u_3
inst_1 : AddCommMonoid U
inst_2 : AddCommMonoid V_1
inst_3 : Module R_1 U
inst_4 : Module R_1 V_1
e : V_1 ≃ₗ[R_1] V_1
P : Submodule R_1 U
Q : Submodule R_1 V_1
R : Type u_4
V : Type u_5
inst_5 : Ring R
inst_6 : AddCommGroup V
inst_7 : Module R V
W : Submodule R V
⊢ Quotient.equiv W W (↑1 : V ≃ₗ[R] V) ⋯ = 1

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R_1 : Type u_1
inst : Semiring R_1
U : Type u_2
V_1 : Type u_3
inst_1 : AddCommMonoid U
inst_2 : AddCommMonoid V_1
inst_3 : Module R_1 U
inst_4 : Module R_1 V_1
e : V_1 ≃ₗ[R_1] V_1
P : Submodule R_1 U
Q : Submodule R_1 V_1
R : Type u_4
V : Type u_5
inst_5 : Ring R
inst_6 : AddCommGroup V
inst_7 : Module R V
W : Submodule R V
u v : ↥(stabilizer (V ≃ₗ[R] V) W)
h :
  ∀ (x : V ⧸ W),
    Eq (α := V ⧸ W) ((Quotient.equiv W W (↑(u * v) : V ≃ₗ[R] V) ⋯ : (a : V ⧸ W) → V ⧸ W) x : V ⧸ W)
      ((Quotient.equiv W W (↑u : V ≃ₗ[R] V) ⋯ * Quotient.equiv W W (↑v : V ≃ₗ[R] V) ⋯ : (a : V ⧸ W) → V ⧸ W) x : V ⧸ W)
⊢ Quotient.equiv W W (↑(u * v) : V ≃ₗ[R] V) ⋯ =
    Quotient.equiv W W (↑u : V ≃ₗ[R] V) ⋯ * Quotient.equiv W W (↑v : V ≃ₗ[R] V) ⋯

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R_1 : Type u_1
inst : Semiring R_1
U : Type u_2
V_1 : Type u_3
inst_1 : AddCommMonoid U
inst_2 : AddCommMonoid V_1
inst_3 : Module R_1 U
inst_4 : Module R_1 V_1
e : V_1 ≃ₗ[R_1] V_1
P : Submodule R_1 U
Q : Submodule R_1 V_1
R : Type u_4
V : Type u_5
inst_5 : Ring R
inst_6 : AddCommGroup V
inst_7 : Module R V
W : Submodule R V
u v : ↥(stabilizer (V ≃ₗ[R] V) W)
x : V ⧸ W
h :
  ∀ (y : V),
    Eq (α := V ⧸ W)
      ((Quotient.equiv W W (↑(u * v) : V ≃ₗ[R] V) ⋯ : (a : V ⧸ W) → V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) y) : V ⧸ W)
      ((Quotient.equiv W W (↑u : V ≃ₗ[R] V) ⋯ * Quotient.equiv W W (↑v : V ≃ₗ[R] V) ⋯ : (a : V ⧸ W) → V ⧸ W)
          ((W.mkQ : (a : V) → V ⧸ W) y) :
        V ⧸ W)
⊢ Eq (α := V ⧸ W) ((Quotient.equiv W W (↑(u * v) : V ≃ₗ[R] V) ⋯ : (a : V ⧸ W) → V ⧸ W) x : V ⧸ W)
    ((Quotient.equiv W W (↑u : V ≃ₗ[R] V) ⋯ * Quotient.equiv W W (↑v : V ≃ₗ[R] V) ⋯ : (a : V ⧸ W) → V ⧸ W) x : V ⧸ W)

Tactic:
obtain ⟨y, rfl⟩ := W.mkQ_surjective x

Premises used: Submodule.mkQ_surjective, rfl
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R_1 : Type u_1
inst : Semiring R_1
U : Type u_2
V_1 : Type u_3
inst_1 : AddCommMonoid U
inst_2 : AddCommMonoid V_1
inst_3 : Module R_1 U
inst_4 : Module R_1 V_1
e : V_1 ≃ₗ[R_1] V_1
P : Submodule R_1 U
Q : Submodule R_1 V_1
R : Type u_4
V : Type u_5
inst_5 : Ring R
inst_6 : AddCommGroup V
inst_7 : Module R V
W : Submodule R V
u v : ↥(stabilizer (V ≃ₗ[R] V) W)
y : V
⊢ Eq (α := V ⧸ W)
    ((Quotient.equiv W W (↑(u * v) : V ≃ₗ[R] V) ⋯ : (a : V ⧸ W) → V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) y) : V ⧸ W)
    ((Quotient.equiv W W (↑u : V ≃ₗ[R] V) ⋯ * Quotient.equiv W W (↑v : V ≃ₗ[R] V) ⋯ : (a : V ⧸ W) → V ⧸ W)
        ((W.mkQ : (a : V) → V ⧸ W) y) :
      V ⧸ W)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
u : ↥(stabilizer (V ≃ₗ[R] V) W)
x : V
⊢ Eq (α := V ⧸ W)
    ((((reduce W : (a : ↥(stabilizer (V ≃ₗ[R] V) W)) → (V ⧸ W) ≃ₗ[R] V ⧸ W) u : (V ⧸ W) ≃ₗ[R] V ⧸ W) :
          (a : V ⧸ W) → V ⧸ W)
        (Submodule.Quotient.mk x) :
      V ⧸ W)
    (Submodule.Quotient.mk (((↑u : V ≃ₗ[R] V) : (a : V) → V) x) : V ⧸ W)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
u : ↥(stabilizer (V ≃ₗ[R] V) W)
x : V
⊢ Eq (α := V ⧸ W)
    ((((reduce W : (a : ↥(stabilizer (V ≃ₗ[R] V) W)) → (V ⧸ W) ≃ₗ[R] V ⧸ W) u : (V ⧸ W) ≃ₗ[R] V ⧸ W) :
          (a : V ⧸ W) → V ⧸ W)
        ((W.mkQ : (a : V) → V ⧸ W) x) :
      V ⧸ W)
    ((W.mkQ : (a : V) → V ⧸ W) (((↑u : V ≃ₗ[R] V) : (a : V) → V) x) : V ⧸ W)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
x : V
⊢ Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
    ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        (Submodule.Quotient.mk x) :
      V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
    (Submodule.Quotient.mk ((e : (a : V) → V) x) : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
x : V
⊢ Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
    ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x) :
      V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
    (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) ((e : (a : V) → V) x) :
      V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
simp :
  (∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
      (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x) ↔
    ∀ (v : V),
      Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
            (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
⊢ (∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
      (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x) ↔
    ∀ (v : V), HSub.hSub (α := V) ((e : (a : V) → V) v : V) (a • v) ∈ (↑e : V →ₗ[R] V).fixedSubmodule

Tactic:
simp only [← e.fixedSubmodule.ker_mkQ, mem_ker, map_sub, ← fixedReduce_mkQ, sub_eq_zero]

Premises used: map_sub, sub_eq_zero, LinearMap.mem_ker, LinearEquiv.toLinearMap, LinearMap.fixedSubmodule, Submodule.ker_mkQ, LinearEquiv.fixedReduce_mkQ
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
mp :
  (∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
      (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x) →
    ∀ (v : V),
      Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
            (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
mpr :
  (∀ (v : V),
      Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
            (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)) →
    ∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
      (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x
⊢ (∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
      (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x) ↔
    ∀ (v : V),
      Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
            (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
H :
  ∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
    (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x
x : V
⊢ Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
    ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x) :
      V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
    (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • x) :
      V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)

Tactic:
simp [H]
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
H :
  ∀ (v : V),
    Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
          (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule
mpr :
  ∀ (y : V) (hy : ((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y = x),
    (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x
⊢ (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x

Tactic:
have ⟨y, hy⟩ := e.fixedSubmodule.mkQ_surjective x
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
H :
  ∀ (v : V),
    Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
          (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule
y : V
hy : ((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y = x
mpr :
  (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y) =
    HSMul.hSMul (β := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) a
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
⊢ (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x

Tactic:
rw [← hy]
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
H :
  ∀ (v : V),
    Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
          (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule
y : V
hy : ((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y = x
⊢ (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y) =
    HSMul.hSMul (β := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) a
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)

Tactic:
apply H
-- Module: Mathlib.LinearAlgebra.FixedSubmodule
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
⊢ e.fixedReduce = refl R (V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) ↔
    ∀ (v : V), HSub.hSub (α := V) ((e : (a : V) → V) v : V) v ∈ (↑e : V →ₗ[R] V).fixedSubmodule

Tactic:
simpa [LinearEquiv.ext_iff] using fixedReduce_eq_smul_iff e 1

Premises used: LinearEquiv.fixedReduce_eq_smul_iff, LinearEquiv.ext_iff, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
X : Type v
inst : CommSemiring R
⊢ Free R (FreeAlgebra R X)

Tactic:
.of_equiv equivMonoidAlgebraFreeMonoid.symm.toLinearEquiv

Premises used: AlgEquiv.symm, Module.Free.of_equiv, AlgEquiv.toLinearEquiv, FreeAlgebra.equivMonoidAlgebraFreeMonoid