mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ {t | t ⊆ s} = s.powerset

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
k : ℕ
⊢ {s | #s = k} = powersetCard k univ

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite

Tactic:
refine ⟨range (Subtype.val ∘ f), ?_, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ range (Subtype.val ∘ f) ⊆ s

case refine_2
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Countable

case refine_3
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Infinite
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
⊢ ∀ (t : { t // (f t).Nonempty }), ∃ x, ↑x ∈ f ↑t

Tactic:
rintro ⟨t, ⟨x, hx⟩⟩

Goal state after:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
t : β
x : α
hx : x ∈ f t
⊢ ∃ x_1, ↑x_1 ∈ f ↑⟨t, ⋯⟩
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ Ici x = {y | ¬y < x}

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ Iic x = {y | ¬x < y}

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
⊢ (e₁.sumCongr e₂).trans (f₁.sumCongr f₂) = (e₁.trans f₁).sumCongr (e₂.trans f₂)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
⊢ (refl α).sumCongr (refl β) = refl (α ⊕ β)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: case mk
ι : Type u
f : ι → Cardinal.{v}
α : Type v
⊢ lift.{u, v} #α ^ sum f = prod fun i ↦ #α ^ f i

Tactic:
induction f using induction_on_pi with

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
⊢ (e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂) = (e₁.trans f₁).sumLexCongr (e₂.trans f₂)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
⊢ (refl α).sumLexCongr (refl β) = refl (α ⊕ₗ β)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
c : Chain α
⊢ c.map OrderHom.id = c

Tactic:
ext; simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case mk
α : Type u
f : Set α → α
hf : Injective f
⊢ False

Tactic:
exact cantor_injective f hf

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
⊢ False

Tactic:
by
      let ι := { c : Cardinal // ¬Acc (· < ·) c }
      let f : ι → Cardinal := Subtype.val
      have hι : Nonempty ι := ⟨⟨_, h⟩⟩
      obtain ⟨⟨c : Cardinal, hc : ¬Acc (· < ·) c⟩, ⟨h_1 : ∀ j, (f ⟨c, hc⟩).out ↪ (f j).out⟩⟩ :=
        Embedding.min_injective fun i => (f i).out
      refine hc (Acc.intro _ fun j h' => by_contradiction fun hj => h'.2 ?_)
      have : #_ ≤ #_ := ⟨h_1 ⟨j, hj⟩⟩
      simpa only [mk_out] using this

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
c : Cardinal.{u}
f : α → β
hf : ∀ (b : β), #↑(f ⁻¹' {b}) ≤ c
⊢ #α ≤ #β * c

Tactic:
by
  simpa only [← mk_congr (@Equiv.sigmaFiberEquiv α β f), mk_sigma, ← sum_const'] using!
    sum_le_sum _ _ hf

Goal state after:
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : Monoid N
φ : M →* N
ψ : N →* M
h : Function.RightInverse ⇑φ ⇑ψ
χ : M →* M
inst✝ : IsId χ
⊢ ψ.comp φ = χ

Tactic:
by simp only [IsId.eq_id, ← DFunLike.coe_fn_eq, coe_comp, h.id, coe_id]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : 1 • a = 1 • b
⊢ a = b

Tactic:
rw [one_smul, one_smul] at ab

Goal state after:
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : a = b
⊢ a = b
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬sSup s ≤ d
⊢ False

Tactic:
rw [csSup_le_iff' hs] at h

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬∀ x ∈ s, x ≤ d
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
by
  rw [lift_iSup hf]
  exact ciSup_le_iff' (bddAbove_range_comp.{_, _, u} hf _)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 0 • a < ℵ₀ ↔ 0 = 0 ∨ a < ℵ₀

Tactic:
by simpa using aleph0_pos

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ Nonempty ↑s ↔ s.Nonempty

Tactic:
nonempty_coe_sort

Goal state after:
α : Type u
s : Set α
⊢ s.Nonempty ↔ s.Nonempty
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : MulAction (M × N) α
instM : MulAction M α := compHom α (MonoidHom.inl M N)
instN : MulAction N α := compHom α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ ((m, 1) * (1, n)) • a = ((1, n) * (m, 1)) • a

Tactic:
Prod.mk_mul_mk,

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : MulAction (M × N) α
instM : MulAction M α := compHom α (MonoidHom.inl M N)
instN : MulAction N α := compHom α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ (m * 1, 1 * n) • a = (1 * m, n * 1) • a
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ ((m, 1) * (1, n)) • a = SMul.smul (m, n) a

Tactic:
Prod.mk_mul_mk,

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ (m * 1, 1 * n) • a = SMul.smul (m, n) a
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ Function.LeftInverse
    (fun _insts ↦
      have this := ⋯;
      prodOfSMulCommClass M N α)
    fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩

Tactic:
rintro ⟨_⟩; dsimp only; ext ⟨m, n⟩ a
    change (m, (1 : N)) • ((1 : M), n) • a = _
    rw [← mul_smul, Prod.mk_mul_mk, mul_one, one_mul]; rfl

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
⊢ ↑e₁₂ ∘ₛₗ ↑e₁₂.symm ∘ₛₗ f = f

Tactic:
ext; simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₁] M₁
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
⊢ ↑e₁₂.symm ∘ₛₗ ↑e₁₂ ∘ₛₗ f = f

Tactic:
ext; simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
⊢ ↑e ∘ₛₗ ↑e.symm ∘ₛₗ f = f

Tactic:
ext; simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₁] M₁
⊢ ↑e.symm ∘ₛₗ ↑e ∘ₛₗ f = f

Tactic:
ext; simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ →ₛₗ[σ₂₃] M₃
⊢ (f ∘ₛₗ ↑e) ∘ₛₗ ↑e.symm = f

Tactic:
ext; simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ →ₛₗ[σ₁₃] M₃
⊢ (f ∘ₛₗ ↑e.symm) ∘ₛₗ ↑e = f

Tactic:
ext; simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ ≃ₛₗ[σ₁₃] M₃
⊢ e.trans (e.symm.trans f) = f

Tactic:
ext; simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ ≃ₛₗ[σ₂₃] M₃
⊢ e.symm.trans (e.trans f) = f

Tactic:
ext; simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₁] M₁
⊢ (f.trans e).trans e.symm = f

Tactic:
ext; simp

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₂] M₂
⊢ (f.trans e.symm).trans e = f

Tactic:
ext; 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✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝³ : DistribSMul S M₂
inst✝² : SMulCommClass R₂ S M₂
inst✝¹ : DistribSMul T M₂
inst✝ : SMulCommClass R₂ T M₂
a : S
f : M →ₛₗ[σ₁₂] M₂
c : R
x : M
⊢ (a • ⇑f) (c • x) = σ₁₂ c • (a • ⇑f) x

Tactic:
simp [Pi.smul_apply, smul_comm]

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

Goal state before:
pp: S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst✝¹⁵ : Semiring R
inst✝¹⁴ : Semiring S
inst✝¹³ : AddCommMonoid V
inst✝¹² : Module R V
inst✝¹¹ : Module S V
inst✝¹⁰ : AddCommMonoid W
inst✝⁹ : Module R W
inst✝⁸ : Module S W
inst✝⁷ : AddCommMonoid G
inst✝⁶ : Module R G
inst✝⁵ : Module S G
inst✝⁴ : SMulCommClass R S W
inst✝³ : SMul S R
inst✝² : IsScalarTower S R V
inst✝¹ : IsScalarTower S R W
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
⊢ e ≪≫ₗ (α • f) = α • e ≪≫ₗ f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ Function.Injective fun a ↦ ↑n • a

Tactic:
apply smul_right_injective

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ ((m, 1) * (1, n)) • a = SMul.smul (m, n) a

Tactic:
Prod.mk_mul_mk,

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ (m * 1, 1 * n) • a = SMul.smul (m, n) a
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
⊢ f.smulRight 0 = 0

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : M
⊢ smulRight 0 x = 0

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ Commute LinearMap.id f

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ Commute f LinearMap.id

Tactic:
ext; simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a : S
⊢ a • 0 = 0

Tactic:
ext; simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a : ↥p
⊢ 0 • a = 0

Tactic:
ext; simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : ↥t
⊢ 1 • x✝ = x✝

Tactic:
ext; simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : S
⊢ x✝ • 0 = 0

Tactic:
ext; simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : ↥t
⊢ 0 • x✝ = 0

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
R₂✝ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁✝ : Type u_6
M₂✝ : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst✝¹⁹ : Semiring R₁
inst✝¹⁸ : Semiring R₂
inst✝¹⁷ : Semiring R₁'
inst✝¹⁶ : Semiring 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₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁵ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝⁴ : RingHomInvPair σ₂'₁' σ₁'₂'
inst✝³ : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst✝² : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst✝¹ : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst✝ : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₂ →ₛₗ[σ₂₂'] M₂'
x : M₂
⊢ ((fun f ↦ (↑e₂ ∘ₛₗ f) ∘ₛₗ ↑e₁.symm) ((fun f ↦ (↑e₂.symm ∘ₛₗ f) ∘ₛₗ ↑e₁) f)) x = f x

Tactic:
simp only [Function.comp_apply, apply_symm_apply, coe_comp, coe_coe]

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

Goal state before:
pp: R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
q : Submodule R₂ M₂
f g : M →ₛₗ[σ₁₂] M₂
hf : MapsTo ⇑f ↑p ↑q
hg : MapsTo ⇑g ↑p ↑q
hfg : MapsTo ⇑(f - g) ↑p ↑q
⊢ f.restrict hf - g.restrict hg = (f - g).restrict hfg

Tactic:
ext; simp

Goal state after: