mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: case pred
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S✝ : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_14
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
n : ℕ
ih : fₗ (-↑n • x) = -↑n • fₗ x
⊢ fₗ ((-↑n - 1) • x) = (-↑n - 1) • fₗ x

Tactic:
simp [sub_smul]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
⊢ Injective toNatLinearMap

Tactic:
intro f g h
  ext x
  exact LinearMap.congr_fun h x

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
⊢ Injective toIntLinearMap

Tactic:
intro f g h
  ext x
  exact LinearMap.congr_fun h x

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
⊢ f.trans f.symm = refl R₁ M₁

Tactic:
by
  ext x
  simp

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₁
inst✝ : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
⊢ f.symm.trans f = refl R₂ M₂

Tactic:
by
  ext x
  simp

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
r : R₁
x : M
⊢ (⇑f - ⇑g) (r • x) = σ₁₂ r • (⇑f - ⇑g) x

Tactic:
by simp [Pi.sub_apply, smul_sub]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝¹⁴ : Monoid M
N : Type u_2
inst✝¹³ : Monoid N
P : Type u_3
inst✝¹² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝¹¹ : Monoid A
inst✝¹⁰ : MulDistribMulAction M A
B : Type u_5
inst✝⁹ : Monoid B
inst✝⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝⁷ : Monoid B₁
inst✝⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝⁵ : Monoid C
inst✝⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝³ : Group A'
inst✝² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹ : Group B'
inst✝ : MulDistribMulAction N B'
f g : A →ₑ*[φ] B
h : (fun m ↦ m.toFun) f = (fun m ↦ m.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨tF, _, _⟩; rcases g with ⟨tG, _, _⟩
    cases tF; cases tG; congr

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : AddZeroClass M
inst✝² : AddZeroClass N
inst✝¹ : DistribSMul R M
inst✝ : DistribSMul R N
x✝² : R
x✝¹ x✝ : M × N
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
by ext <;> exact smul_add ..

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Injective ⇑(f' ^ n)
⊢ 0 < n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
ι : Sort u_9
f : M →ₛₗ[σ₁₂] M₂
p : ι → Submodule R₂ M₂
⊢ comap f (⨅ i, p i) = ⨅ i, comap f (p i)

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ x✝ ∈ map (↑e) K ↔ x✝ ∈ comap (↑e.symm) K

Tactic:
by rw [mem_map_equiv, mem_comap, LinearEquiv.coe_coe]

Goal state after:
Module: Mathlib.Data.Int.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑↑x✝, ↑↑x✝) = ↑x✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Data.Int.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑(Int.negSucc x✝), ↑(Int.negSucc x✝)) = -↑(x✝ + 1)

Tactic:
ext <;> simp

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝ : M₀
⊢ 0 * x✝ = x✝ * 0

Tactic:
zero_mul,

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝ : M₀
⊢ 0 = x✝ * 0
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 * (x✝¹ * x✝) = 0 * x✝¹ * x✝

Tactic:
zero_mul,

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 = 0 * x✝¹ * x✝
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 = 0 * x✝¹ * x✝

Tactic:
zero_mul,

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 = 0 * x✝
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 * ↑u = ↑u * 0

Tactic:
zero_mul,

Goal state after:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 = ↑u * 0
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 * (x✝¹ * x✝) = 0 * x✝¹ * x✝

Tactic:
zero_mul,

Goal state after:
case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 = 0 * x✝¹ * x✝
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 = 0 * x✝¹ * x✝

Tactic:
zero_mul,

Goal state after:
case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 = 0 * x✝
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ srange f = map f ⊤

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * x - (algebraMap R A) r * x = (x - (algebraMap R A) r) * x

Tactic:
sub_mul

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * x - (algebraMap R A) r * x = x * x - (algebraMap R A) r * x
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
⊢ f.rangeS = Subsemiring.map f ⊤

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ x✝² • (algebraMap R A) x✝¹ + x✝² • (algebraMap R A) x✝ = (algebraMap R A) (x✝² • x✝¹ + x✝² • x✝)

Tactic:
← algebraMap.smul',

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ (algebraMap R A) (x✝² • x✝¹) + x✝² • (algebraMap R A) x✝ = (algebraMap R A) (x✝² • x✝¹ + x✝² • x✝)
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ (algebraMap R A) (x✝² • x✝¹) + x✝² • (algebraMap R A) x✝ = (algebraMap R A) (x✝² • x✝¹ + x✝² • x✝)

Tactic:
← algebraMap.smul',

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ (algebraMap R A) (x✝² • x✝¹) + (algebraMap R A) (x✝² • x✝) = (algebraMap R A) (x✝² • x✝¹ + x✝² • x✝)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
⊢ f.range = Subring.map f ⊤

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List R
HL' : ∀ x ∈ L, x ∈ s
⊢ C (-L.prod)

Tactic:
induction L with
    | nil => exact hneg1
    | cons hd tl ih =>
      rw [List.prod_cons, neg_mul_eq_mul_neg]
      rw [List.forall_mem_cons] at HL'
      exact hs _ HL'.1 _ (ih HL'.2)

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

Goal state before:
pp: M : Type u_1
inst✝ : MonoidWithZero M
a : M
h✝ : a ~ᵤ 0
u : Mˣ
h : 0 * ↑u = a
⊢ a = 0

Tactic:
simpa using h.symm

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
⊢ ∀ (a b : M), p * ↑u ∣ a * b → p * ↑u ∣ a ∨ p * ↑u ∣ b

Tactic:
simp only [Units.isUnit, IsUnit.mul_right_dvd]

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
⊢ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ 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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.range = map f ⊤

Tactic:
ext
  simp

Goal state after:
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₂
p : Submodule R₂ M₂
⊢ f.range ≤ p ↔ comap f p = ⊤

Tactic:
rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ ((-id) ∘ₛₗ f).range = f.range

Tactic:
range_comp,

Goal state after:
R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ map (-id) f.range = f.range
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₂
⊢ (↑e).comp ↑e.symm = AlgHom.id R A₂

Tactic:
ext
  simp

Goal state after:
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₂
⊢ (↑e.symm).comp ↑e = AlgHom.id R A₁

Tactic:
ext
  simp

Goal state after:
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₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
⊢ (e₁.arrowCongr e₃) (g.comp f) = ((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)

Tactic:
ext
  simp

Goal state after:
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✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
⊢ (fun ψ ↦ e.trans (ψ.trans e'.symm)) ((fun ψ ↦ e.symm.trans (ψ.trans e')) ψ) = ψ

Tactic:
by
    ext
    simp_rw [trans_apply, symm_apply_apply]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : RingHomSurjective τ₂₃
inst✝ : RingHomSurjective τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : f.range = ⊤
⊢ (g ∘ₛₗ f).range = g.range

Tactic:
range_comp,

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : RingHomSurjective τ₂₃
inst✝ : RingHomSurjective τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : f.range = ⊤
⊢ Submodule.map g f.range = g.range
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective ⇑i
hf : ∀ (x : M₁), f x ∈ i.range
⊢ i ∘ₗ f.codRestrictOfInjective i hi hf = f

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
hNO : N ≤ O
⊢ Submodule.map ϕ (Submodule.comap O.subtype N) = (ϕ ∘ₗ Submodule.inclusion hNO).range

Tactic:
range_comp,

Goal state after:
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
hNO : N ≤ O
⊢ Submodule.map ϕ (Submodule.comap O.subtype N) = Submodule.map ϕ (Submodule.inclusion hNO).range
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case inl
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
r✝ : S
n✝ : M
hr : r✝ ∈ s
hn : n✝ ∈ N
⊢ r✝ • n✝ ∈ s • N ⊔ t • N

pp: case inr
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
r✝ : S
n✝ : M
hr : r✝ ∈ t
hn : n✝ ∈ N
⊢ r✝ • n✝ ∈ s • N ⊔ t • N

Tactic:
· exact Submodule.mem_sup_left (mem_set_smul_of_mem_mem hr hn)

Goal state after:
case inr
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
r✝ : S
n✝ : M
hr : r✝ ∈ t
hn : n✝ ∈ N
⊢ r✝ • n✝ ∈ s • N ⊔ t • N
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ c = ofPred (⇑c) c.IsClosed ⋯ ⋯ ⋯

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_9
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
g : G
x : M
⊢ R ∙ x ≤ R ∙ g • x

Tactic:
convert! span_singleton_smul_le R g⁻¹ (g • x)

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_9
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
g : G
x : M
⊢ x = g⁻¹ • g • x
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl.inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊥
⊢ ⊥ ≠ ⊤

Tactic:
simpa using h.symm

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊥
⊢ ⊥ ≠ ⊤

Tactic:
simpa using h.symm

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤

Tactic:
simpa using h.symm

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ span R (range (update v j (v j + r • v i))) = span R (range v)

Tactic:
refine le_antisymm ?_ ?_ <;> simp only [span_le, Set.range_subset_iff, SetLike.mem_coe] <;>
    intro k

Goal state after:
case refine_1
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
⊢ update v j (v j + r • v i) k ∈ span R (range v)

case refine_2
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
⊢ v k ∈ span R (range (update v j (v j + r • v i)))
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
s : Set α
⊢ IsAtom s ↔ ∃ x, s = {x}

Tactic:
refine
    ⟨?_, by
      rintro ⟨x, rfl⟩
      exact isAtom_singleton x⟩

Goal state after:
α : Type u_2
s : Set α
⊢ IsAtom s → ∃ x, s = {x}
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
j : ι
hj : j ≠ k
⊢ t j = t i

Tactic:
rw [(huniv j).resolve_right hj]

Goal state after:
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: S : Type u
A : Type v
inst✝¹ : CommSemiring S
inst✝ : Semiring A
h1 h2 : Algebra S A
h :
  ∀ (r : S) (x : A),
    (have I := h1;
      r • x) =
      r • x
r : S
⊢ (algebraMap S A) r = (algebraMap S A) r

Tactic:
simpa only [@Algebra.smul_def _ _ _ _ h1, @Algebra.smul_def _ _ _ _ h2, mul_one] using h r 1

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), IsCompactElement c → c ≤ a → c ≤ b
⊢ a ≤ b

Tactic:
← sSup_compact_le_eq a,

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), IsCompactElement c → c ≤ a → c ≤ b
⊢ sSup {c | IsCompactElement c ∧ c ≤ a} ≤ b
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R (r • s) ≤ span R s

pp: case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R s ≤ span R (r • s)

Tactic:
· apply span_smul_le

Goal state after:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R s ≤ span R (r • s)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
h : x ∈ span R s
⊢ f x ∈ span R₂ (⇑f '' s)

Tactic:
rw [Submodule.span_image]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
h : x ∈ span R s
⊢ f x ∈ map f (span R s)
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_8
inst✝ : NonAssocSemiring R
x : ι → R
⊢ x = ∑ i, x i • fun j ↦ if i = j then 1 else 0

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
x✝ : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).1 + (x₁, x₂).2 = ↑l
⊢ ∃ a, a ≤ (x₁, x₂).1 + (x₁, x₂).2 ∧ (a, (x₁, x₂).1 + (x₁, x₂).2 - a) = (x₁, x₂)

Tactic:
exact ⟨x₁, le_add_right _ _, by rw [add_tsub_cancel_left x₁ x₂]⟩

Goal state after: