mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
ι : Type v
f : ι → Set α
⊢ (sum fun i ↦ #↑(f i)) = sum fun i ↦ #↑(f i)

Tactic:
]

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

Goal state before:
pp: α : Type u
A : Set (Set α)
⊢ #↑(⋃ i, ↑i) ≤ #↑A * ⨆ s, #↑↑s

Tactic:
]

Goal state after:
α : Type u
A : Set (Set α)
⊢ #↑(⋃ i, ↑i) ≤ #↑A * ⨆ s, #↑↑s
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ x, A ↑x) ≤ #↑s * ⨆ x, #↑(A ↑x)

Tactic:
]

Goal state after:
ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ x, A ↑x) ≤ #↑s * ⨆ x, #↑(A ↑x)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
ι : Type v
A : ι → Set α
s : Set ι
⊢ lift.{v, u} #↑(⋃ x, A ↑x) ≤ lift.{u, v} #↑s * ⨆ x, lift.{v, u} #↑(A ↑x)

Tactic:
]

Goal state after:
α : Type u
ι : Type v
A : ι → Set α
s : Set ι
⊢ lift.{v, u} #↑(⋃ x, A ↑x) ≤ lift.{u, v} #↑s * ⨆ x, lift.{v, u} #↑(A ↑x)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) ↔ ∃ t, ↑t = univ ∧ t.card = n

Tactic:
]

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) ↔ ∃ h, Fintype.card α = n

Tactic:
]

Goal state after:
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) ↔ ∃ h, Fintype.card α = n
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
]

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

Goal state before:
pp: α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑s + 1 = #↑s + 1

pp: α : Type u
s : Set α
a : α
h : a ∉ s
⊢ Disjoint s {a}

Tactic:
]

Goal state after:
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ Disjoint s {a}
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑s + 1 ≤ #↑s + 1

Tactic:
]

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

Goal state before:
pp: α : Type u
S T : Set α
h : T ⊆ S
⊢ #↑S = #↑S

Tactic:
]

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

Goal state before:
pp: α : Type u
S T : Set α
h : #↑S < #↑T
⊢ #↑(T \ S) ≠ 0

Tactic:
]

Goal state after:
α : Type u
S T : Set α
h : #↑S < #↑T
⊢ #↑(T \ S) ≠ 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S : Set α
h : #↑S < #↑univ
⊢ Sᶜ.Nonempty

Tactic:
]

Goal state after:
α : Type u
S : Set α
h : #↑S < #↑univ
⊢ Sᶜ.Nonempty
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Nonempty (↑(f ⁻¹' s) ↪ ↑s)

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Nonempty (↑(f ⁻¹' s) ↪ ↑s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : f '' f ⁻¹' s = s
⊢ lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : f '' f ⁻¹' s = s
⊢ lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case e'_2
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑(f ⁻¹' s) = #↑(f ⁻¹' s)

Tactic:
]

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

Goal state before:
pp: case e'_3
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑s = #↑s

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ univ

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ univ
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ lift.{u, u} #↑(f ⁻¹' s) ≤ lift.{u, u} #↑s

Tactic:
]

Goal state after:
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ lift.{u, u} #↑(f ⁻¹' s) ≤ lift.{u, u} #↑s
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, u} #↑s ≤ lift.{u, u} #↑(f ⁻¹' s)

Tactic:
]

Goal state after:
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, u} #↑s ≤ lift.{u, u} #↑(f ⁻¹' s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ lift.{u, v} #↑t ≤ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ lift.{u, v} #↑t ≤ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t}
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ lift.{v, u} #↑{x | f ↑x ∈ t} = lift.{v, u} #↑((fun x ↦ f ↑x) ⁻¹' t)

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ lift.{v, u} #↑{x | f ↑x ∈ t} = lift.{v, u} #↑((fun x ↦ f ↑x) ⁻¹' t)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
]

Goal state after:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑{x | f ↑x ∈ t} = #↑((fun x ↦ f ↑x) ⁻¹' t)

Tactic:
]

Goal state after:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑{x | f ↑x ∈ t} = #↑((fun x ↦ f ↑x) ⁻¹' t)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
⊢ (∃ p, #↑p = c) ↔ ∃ s_1, #↑(Subtype.val '' s_1) = c

Tactic:
]

Goal state after:
c : Cardinal.{u}
α : Type u
s : Set α
⊢ (∃ p, #↑p = c) ↔ ∃ s_1, #↑(Subtype.val '' s_1) = c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ #↑t = c ↔ #↑t = c

pp: c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ Injective Subtype.val

Tactic:
]

Goal state after:
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ Injective Subtype.val
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
⊢ lift.{v, u} #α = lift.{v, u} #α

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
⊢ lift.{u, v} #β = lift.{u, v} #β

Tactic:
]

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

Goal state before:
pp: α : Type u
⊢ (∃ x y, x ≠ y) ↔ ∃ x y, x ≠ y

Tactic:
]

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

Goal state before:
pp: α : Type u
x : α
⊢ (∃ y, y ≠ x) ↔ ∃ y, y ≠ x

Tactic:
]

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

Goal state before:
pp: α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x

Tactic:
]

Goal state after:
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ↑(2 + 1) ≤ #α

Tactic:
]

Goal state after:
α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ↑(2 + 1) ≤ #α
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)

Tactic:
]

Goal state after:
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b c : Cardinal.{u}
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ x < b, a ^ x ≤ c

pp: case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)

Tactic:
]

Goal state after:
a b c : Cardinal.{u}
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ x < b, a ^ x ≤ c

case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case h
a b c : Cardinal.{u}
⊢ BddAbove (HPow.hPow a '' Iio b)

Tactic:
]

Goal state after:
case h
a b c : Cardinal.{u}
⊢ BddAbove (HPow.hPow a '' Iio b)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
h : a ≠ 0
⊢ ?m.23 ^ 0 ≤ 0 ^< a

pp: a : Cardinal.{u_1}
h : a ≠ 0
⊢ Cardinal.{u_1}

Tactic:
]

Goal state after:
a : Cardinal.{u_1}
h : a ≠ 0
⊢ ?m.23 ^ 0 ≤ 0 ^< a

a : Cardinal.{u_1}
h : a ≠ 0
⊢ Cardinal.{u_1}
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • x = r • x

Tactic:
]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
r : R
a : A
⊢ (algebraMap R A) r * a = (algebraMap R A) r * a

Tactic:
]

Goal state after:
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
inst✝² : MulAction M α
inst✝¹ : MulAction N α
inst✝ : SMulCommClass M N α
x y : M × N
a : α
⊢ x.1 • x.2 • y.1 • y.2 • a = x.1 • x.2 • y.1 • y.2 • a

Tactic:
]

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ (algebraMap R A) r * (x * y) = (algebraMap R A) r * (x * y)

Tactic:
]

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * y * (algebraMap R A) r = x * y * (algebraMap R A) r

Tactic:
]

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : R
y z : A
⊢ (algebraMap R A) x * (y * z) = (algebraMap R A) x * (y * z)

Tactic:
]

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : R
x y : A
⊢ (algebraMap R A) s * (x * y) = (algebraMap R A) s * (x * y)

Tactic:
]

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

Goal state before:
pp: R : Type u
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
α : Type u_2
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ r • 1 = r • 1

Tactic:
]

Goal state after:
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, n) • a = SMul.smul (m, n) a

Tactic:
]

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, n) • a = SMul.smul (m, n) a
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: G : Type u_1
R : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Monoid R
inst✝³ : AddGroup R
inst✝² : DistribMulAction G R
inst✝¹ : IsScalarTower G R R
inst✝ : SMulCommClass G R R
r : G
a : R
⊢ IsUnit (r • 1 - a) ↔ IsUnit (r • 1 - a)

Tactic:
]

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

Goal state before:
pp: case neg
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this✝ : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
this : h • b ≠ 0
⊢ (g / h * h) • (a / b * b) = g • a

Tactic:
]

Goal state after:
case neg
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this✝ : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
this : h • b ≠ 0
⊢ (g / h * h) • (a / b * b) = g • a
Module: Mathlib.Algebra.Ring.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
n : ℕ
⊢ op ↑n = op ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoidWithOne R
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S : Type u_6
M : 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✝¹⁰ : Semiring R₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : Semiring R₄
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid M₄
inst✝¹ : AddCommMonoid N₁
inst✝ : AddCommMonoid N₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e✝ e' e : M ≃ₛₗ[σ] M₂
r : S
x : M₂
⊢ σ' r • ((↑e).inverse e.invFun ⋯ ⋯) x = σ' r • ((↑e).inverse e.invFun ⋯ ⋯) x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
x✝¹ : M →+ M₂
x✝ : M
⊢ x✝¹ (DomMulAct.mk.symm 0 • x✝) = 0 x✝

Tactic:
]

Goal state after:
R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
x✝¹ : M →+ M₂
x✝ : M
⊢ x✝¹ (DomMulAct.mk.symm 0 • x✝) = 0 x✝
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_14
M : Type u_15
M₂ : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R M₂
F : Type u_17
inst✝¹ : FunLike F M M₂
inst✝ : LinearMapClass F R M M₂
f : F
r : R
x : M
⊢ r • f x = r • f x

Tactic:
]

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
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
⊢ σ 0 • f 0 = 0

Tactic:
]

Goal state after:
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
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
⊢ σ 0 • f 0 = 0
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
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
c : R
x : M
⊢ σ c • f x = σ c • f x

Tactic:
]

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 S✝
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : Module R✝ M
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module S✝ M₃
σ : R✝ →+* S✝
fₗ✝ : M →ₗ[R✝] M₂
f g : M →ₛₗ[σ] M₃
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S M₂
fₗ : M →ₗ[S] M₂
c : R
x : M
⊢ (c • 1) • fₗ x = (c • 1) • fₗ x

Tactic:
]

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₂
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : CompatibleSMul M M₂ R S
inst✝ : IsScalarTower R S M₂
f : M →ₗ[S] M₂
hf : Injective ⇑f
r : R
s : S
x✝ : M
⊢ r • s • f x✝ = r • s • f x✝

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M₃ : Type u_11
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M₃
inst✝ : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : f 1 = g 1
x : R
⊢ σ x • g 1 = σ x • g 1

Tactic:
]

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
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₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
hf : Injective ⇑f
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f ∘ₛₗ g₁ = f ∘ₛₗ g₂
x : M₁
⊢ f (g₂ x) = f (g₂ x)

Tactic:
]

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₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f g : M₃ →ₛₗ[σ₃₁] M₁
h : ↑e₁₂ ∘ₛₗ f = ↑e₁₂ ∘ₛₗ g
⊢ ↑e₁₂ ∘ₛₗ f = ↑e₁₂ ∘ₛₗ f

Tactic:
]

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₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
h : f ∘ₛₗ ↑e₁₂ = g ∘ₛₗ ↑e₁₂
⊢ f ∘ₛₗ ↑e₁₂ = f ∘ₛₗ ↑e₁₂

Tactic:
]

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 S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (f x) = x
h₂ : ∀ (x : M₂), f (g x) = x
x y : M₂
⊢ g (f (g (x + y))) = g (f (g x + g y))

Tactic:
]

Goal state after:
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✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (f x) = x
h₂ : ∀ (x : M₂), f (g x) = x
x y : M₂
⊢ g (f (g (x + y))) = g (f (g x + g y))
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 S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (f x) = x
h₂ : ∀ (x : M₂), f (g x) = x
a : S
b : M₂
⊢ g (f (g (a • b))) = g (f (σ' a • g b))

Tactic:
]

Goal state after:
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✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (f x) = x
h₂ : ∀ (x : M₂), f (g x) = x
a : S
b : M₂
⊢ g (f (g (a • b))) = g (f (σ' a • g b))
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
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 σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
⊢ 0 = 0

Tactic:
]

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 σ₁₂ σ₂₃ σ₁₃
inst✝ : Subsingleton M
f : M →ₛₗ[σ₁₂] M₂
x : M
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: M' : Type u_1
X : Type u_5
inst✝⁶ : SMul M' X
Y : Type u_6
inst✝⁵ : SMul M' Y
F : Type u_8
inst✝⁴ : FunLike F X Y
inst✝³ : MulOneClass X
inst✝² : SMul X Y
inst✝¹ : IsScalarTower M' X Y
inst✝ : MulActionHomClass F X X Y
f : F
m : M'
x : X
⊢ m • f x = m • f x

Tactic:
]

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

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝¹ : (i : I) → g i
x✝ : I
⊢ 0 x✝ = 0 x✝

Tactic:
]

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

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ g (φ m • f x) = g (φ m • f x)

Tactic:
]

Goal state after: