mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a c : M
d : Mˣ
⊢ a * c ~ᵤ a * ↑d * c

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a c : M
d : Mˣ
⊢ a * c ~ᵤ a * ↑d * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case neg
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
⊢ a ~ᵤ a * c

Tactic:
have hac0 : a * c ≠ 0 := by
    intro con
    rw [con, zero_mul] at a_eq
    apply ha0 a_eq

Goal state after:
case neg
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a ~ᵤ a * c
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
S : Submonoid M₀
hS : 0 ∉ S
hx : 0 ∈ S
⊢ False

Tactic:
;

Goal state after:
M₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
S : Submonoid M₀
hS : 0 ∉ S
hx : 0 ∈ S
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ y * z ~ᵤ y

Tactic:
exact Or.inr (associated_mul_unit_left _ _ h)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsLeft M₀ ↔ ∀ (x : M₀), r * x = 0 → x = 0

Tactic:
;

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsLeft M₀ ↔ ∀ (x : M₀), r * x = 0 → x = 0
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsRight M₀ ↔ ∀ (x : M₀), x * r = 0 → x = 0

Tactic:
;

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsRight M₀ ↔ ∀ (x : M₀), x * r = 0 → x = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
⊢ b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
⊢ b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ a * b

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ a * b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ b * a

Tactic:
by rw [mul_comm]; exact le_mul_right

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ b_1, ↑a * ↑↑b_1 = ↑b) ↔ ∃ u, a * ↑u = b

Tactic:
;

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ b_1, ↑a * ↑↑b_1 = ↑b) ↔ ∃ u, a * ↑u = b
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
K : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
x✝ : M₂
⊢ x✝ ∈ (f.domRestrict K).range ↔ x✝ ∈ map f K

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
K : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
x✝ : M₂
⊢ x✝ ∈ (f.domRestrict K).range ↔ x✝ ∈ map f K
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
q : Submodule R₂ M₂
x : M
hx : f x ∈ ↑q
⊢ f x ∈ map f (comap f q)

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
q : Submodule R₂ M₂
x : M
hx : f x ∈ ↑q
⊢ f x ∈ map f (comap f q)
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
x✝ : α
⊢ x✝ ∈ 0⁻¹ ↔ x✝ ∈ 0

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
x✝ : α
⊢ x✝ ∈ 0⁻¹ ↔ x✝ ∈ 0
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ comap f ⊥ = ⊤ ↔ f = 0

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ comap f ⊥ = ⊤ ↔ f = 0
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
a✝ : A₁
⊢ (e.trans e.symm) a✝ = refl a✝

Tactic:
;

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
a✝ : A₁
⊢ (e.trans e.symm) a✝ = refl a✝
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
a✝ : A₂
⊢ (e.symm.trans e) a✝ = refl a✝

Tactic:
;

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
a✝ : A₂
⊢ (e.symm.trans e) a✝ = refl a✝
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: case refl
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A₁
inst✝¹² : Semiring A₂
inst✝¹¹ : Semiring A₃
inst✝¹⁰ : Semiring A₁'
inst✝⁹ : Semiring A₂'
inst✝⁸ : Semiring A₃'
inst✝⁷ : Algebra R A₁
inst✝⁶ : Algebra R A₂
inst✝⁵ : Algebra R A₃
inst✝⁴ : Algebra R A₁'
inst✝³ : Algebra R A₂'
inst✝² : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
ι : Type u_1
A : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
i : ι
x✝ : R
__spread✝⁻⁰ : A i ≃+* A i := RingEquiv.cast ⋯
⊢ (RingEquiv.cast ⋯).toFun ((algebraMap R (A i)) x✝) = (algebraMap R (A i)) x✝

Tactic:
;

Goal state after:
case refl
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A₁
inst✝¹² : Semiring A₂
inst✝¹¹ : Semiring A₃
inst✝¹⁰ : Semiring A₁'
inst✝⁹ : Semiring A₂'
inst✝⁸ : Semiring A₃'
inst✝⁷ : Algebra R A₁
inst✝⁶ : Algebra R A₂
inst✝⁵ : Algebra R A₃
inst✝⁴ : Algebra R A₁'
inst✝³ : Algebra R A₂'
inst✝² : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
ι : Type u_1
A : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
i : ι
x✝ : R
__spread✝⁻⁰ : A i ≃+* A i := RingEquiv.cast ⋯
⊢ (RingEquiv.cast ⋯).toFun ((algebraMap R (A i)) x✝) = (algebraMap R (A i)) x✝
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s : Set β
h : s.Nonempty
⊢ 0 • s = 0

Tactic:
by
  simp only [← image_smul, zero_smul, h.image_const, singleton_zero]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
x✝ : α
⊢ x✝ ∈ (a •> s)⁻¹ ↔ x✝ ∈ s⁻¹ <• a⁻¹

Tactic:
;

Goal state after:
case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
x✝ : α
⊢ x✝ ∈ (a •> s)⁻¹ ↔ x✝ ∈ s⁻¹ <• a⁻¹
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : LeftInverse ⇑g ⇑f
x : M
⊢ f x ∈ (f ∘ₗ g - id).ker

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : LeftInverse ⇑g ⇑f
x : M
⊢ f x ∈ (f ∘ₗ g - id).ker
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
x : A₁
x✝ : A₂
⊢ ((↑f).conj (LinearMap.mulLeft R x)) x✝ = (LinearMap.mulLeft R (f x)) x✝

Tactic:
;

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
x : A₁
x✝ : A₂
⊢ ((↑f).conj (LinearMap.mulLeft R x)) x✝ = (LinearMap.mulLeft R (f x)) x✝
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
x : A₁
x✝ : A₂
⊢ ((↑f).conj (LinearMap.mulRight R x)) x✝ = (LinearMap.mulRight R (f x)) x✝

Tactic:
;

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
x : A₁
x✝ : A₂
⊢ ((↑f).conj (LinearMap.mulRight R x)) x✝ = (LinearMap.mulRight R (f x)) x✝
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
x✝ : α
⊢ x✝ ∈ (s <• a)⁻¹ ↔ x✝ ∈ a⁻¹ •> s⁻¹

Tactic:
;

Goal state after:
case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
x✝ : α
⊢ x✝ ∈ (s <• a)⁻¹ ↔ x✝ ∈ a⁻¹ •> s⁻¹
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: case mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
fst✝ snd✝ : A₁
⊢ (↑f).conj (LinearMap.mulLeftRight R (fst✝, snd✝)) = LinearMap.mulLeftRight R (Prod.map ⇑f ⇑f (fst✝, snd✝))

Tactic:
;

Goal state after:
case mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
fst✝ snd✝ : A₁
⊢ (↑f).conj (LinearMap.mulLeftRight R (fst✝, snd✝)) = LinearMap.mulLeftRight R (Prod.map ⇑f ⇑f (fst✝, snd✝))
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: case mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
fst✝ snd✝ : A₁
x✝ : A₂
⊢ ((↑f).conj (LinearMap.mulLeftRight R (fst✝, snd✝))) x✝ = (LinearMap.mulLeftRight R (Prod.map ⇑f ⇑f (fst✝, snd✝))) x✝

Tactic:
;

Goal state after:
case mk
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
fst✝ snd✝ : A₁
x✝ : A₂
⊢ ((↑f).conj (LinearMap.mulLeftRight R (fst✝, snd✝))) x✝ = (LinearMap.mulLeftRight R (Prod.map ⇑f ⇑f (fst✝, snd✝))) x✝
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
inst✝² : CommSemiring R
inst✝¹ : Semiring A₁
inst✝ : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n : ℕ
x✝ : A₁
⊢ (e ^ Nat.zero) x✝ = (⇑e)^[Nat.zero] x✝

Tactic:
;

Goal state after:
R : Type uR
A₁ : Type uA₁
inst✝² : CommSemiring R
inst✝¹ : Semiring A₁
inst✝ : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n : ℕ
x✝ : A₁
⊢ (e ^ Nat.zero) x✝ = (⇑e)^[Nat.zero] x✝
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
inst✝² : CommSemiring R
inst✝¹ : Semiring A₁
inst✝ : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n x✝¹ : ℕ
ih : ⇑(e ^ x✝¹) = (⇑e)^[x✝¹]
x✝ : A₁
⊢ (e ^ x✝¹.succ) x✝ = (⇑e)^[x✝¹.succ] x✝

Tactic:
;

Goal state after:
R : Type uR
A₁ : Type uA₁
inst✝² : CommSemiring R
inst✝¹ : Semiring A₁
inst✝ : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n x✝¹ : ℕ
ih : ⇑(e ^ x✝¹) = (⇑e)^[x✝¹]
x✝ : A₁
⊢ (e ^ x✝¹.succ) x✝ = (⇑e)^[x✝¹.succ] x✝
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x y : A₁ ≃ₐ[R] A₁
z : A₁ˣ
⊢ ↑((x * y) • z) = ↑(x • y • z)

Tactic:
;

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x y : A₁ ≃ₐ[R] A₁
z : A₁ˣ
⊢ ↑((x * y) • z) = ↑(x • y • z)
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ˣ
⊢ ↑(1 • x) = ↑x

Tactic:
;

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ˣ
⊢ ↑(1 • x) = ↑x
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
⊢ ↑(x • 1) = ↑1

Tactic:
;

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
⊢ ↑(x • 1) = ↑1
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
y z : A₁ˣ
⊢ ↑(x • (y * z)) = ↑(x • y * x • z)

Tactic:
;

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
y z : A₁ˣ
⊢ ↑(x • (y * z)) = ↑(x • y * x • z)
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R✝ : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹⁵ : CommSemiring R✝
inst✝¹⁴ : Semiring A₁
inst✝¹³ : Semiring A₂
inst✝¹² : Semiring A₃
inst✝¹¹ : Semiring A₁'
inst✝¹⁰ : Semiring A₂'
inst✝⁹ : Semiring A₃'
inst✝⁸ : Algebra R✝ A₁
inst✝⁷ : Algebra R✝ A₂
inst✝⁶ : Algebra R✝ A₃
inst✝⁵ : Algebra R✝ A₁'
inst✝⁴ : Algebra R✝ A₂'
inst✝³ : Algebra R✝ A₃'
e : A₁ ≃ₐ[R✝] A₂
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ↑1 x = x

Tactic:
;

Goal state after:
R✝ : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹⁵ : CommSemiring R✝
inst✝¹⁴ : Semiring A₁
inst✝¹³ : Semiring A₂
inst✝¹² : Semiring A₃
inst✝¹¹ : Semiring A₁'
inst✝¹⁰ : Semiring A₂'
inst✝⁹ : Semiring A₃'
inst✝⁸ : Algebra R✝ A₁
inst✝⁷ : Algebra R✝ A₂
inst✝⁶ : Algebra R✝ A₃
inst✝⁵ : Algebra R✝ A₁'
inst✝⁴ : Algebra R✝ A₂'
inst✝³ : Algebra R✝ A₃'
e : A₁ ≃ₐ[R✝] A₂
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ↑1 x = x
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₁
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass S R M₁
inst✝³ : SMulCommClass S R M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M₁
inst✝ : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x✝¹ : R
x✝ : M₂
⊢ (e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁)) x✝¹)) x✝ = ((algebraMap R (Module.End S M₂)) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₁
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass S R M₁
inst✝³ : SMulCommClass S R M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M₁
inst✝ : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x✝¹ : R
x✝ : M₂
⊢ (e.conjRingEquiv.toFun ((algebraMap R (Module.End S M₁)) x✝¹)) x✝ = ((algebraMap R (Module.End S M₂)) x✝¹) x✝
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₁
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass S R M₁
inst✝³ : SMulCommClass S R M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M₁
inst✝ : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x✝¹ : R
x✝ : M₂
⊢ (restrictScalars R e) (((algebraMap R (Module.End S M₁)) x✝¹) (↑e.symm x✝)) =
    ((algebraMap R (Module.End S M₂)) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₁
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass S R M₁
inst✝³ : SMulCommClass S R M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M₁
inst✝ : IsScalarTower R S M₂
e : M₁ ≃ₗ[S] M₂
x✝¹ : R
x✝ : M₂
⊢ (restrictScalars R e) (((algebraMap R (Module.End S M₁)) x✝¹) (↑e.symm x✝)) =
    ((algebraMap R (Module.End S M₂)) x✝¹) x✝
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x✝ : ↥p
⊢ ↑((ofEq p p ⋯) x✝) = ↑((refl R ↥p) x✝)

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_5
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x✝ : ↥p
⊢ ↑((ofEq p p ⋯) x✝) = ↑((refl R ↥p) x✝)
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : ↥p
hx : x ∈ q
⊢ (p.subtype.domRestrict q) ⟨x, hx⟩ ∈ map p.subtype q

Tactic:
;

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : ↥p
hx : x ∈ q
⊢ (p.subtype.domRestrict q) ⟨x, hx⟩ ∈ map p.subtype q
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective ⇑f
h : p ≤ f.range
x✝ : ↥p
y : M
hx : f y ∈ p
⊢ ∃ a, (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) a = ⟨f y, hx⟩

Tactic:
;

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective ⇑f
h : p ≤ f.range
x✝ : ↥p
y : M
hx : f y ∈ p
⊢ ∃ a, (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) a = ⟨f y, hx⟩
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
x₁ x₂ : M₁
⊢ ↑e ∘ₗ codRestrict i.range (f (x₁ + x₂)) ⋯ = ↑e ∘ₗ codRestrict i.range (f x₁) ⋯ + ↑e ∘ₗ codRestrict i.range (f x₂) ⋯

Tactic:
;

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
x₁ x₂ : M₁
⊢ ↑e ∘ₗ codRestrict i.range (f (x₁ + x₂)) ⋯ = ↑e ∘ₗ codRestrict i.range (f x₁) ⋯ + ↑e ∘ₗ codRestrict i.range (f x₂) ⋯