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

Goal state before:
pp: α : Type u_3
R : Type u_5
inst✝ : NonAssocSemiring R
s : Finset α
⊢ ↑(#s) = ∑ x ∈ s, 1

Tactic:
rw [Finset.sum_const, Nat.smul_one_eq_cast]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t
⊢ ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Tactic:
intro i hi

Goal state after:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t
i : ι
hi : i ∉ I
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
x : M
hs : LinearIndepOn R _root_.id s
hx : ∀ (r : R), r • x ∈ span R s → r = 0
⊢ ∀ (r : R), r • _root_.id x ∈ span R (_root_.id '' s) → r = 0

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : MulOneClass M
s : Set M
m : M
inst✝ : Nontrivial R
h : (of R M) m ∈ Submodule.span R ↑(Submonoid.closure (⇑(of R M) '' s))
⊢ m ∈ Submonoid.closure s

Tactic:
rw [← MonoidHom.map_mclosure] at h

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : MulOneClass M
s : Set M
m : M
inst✝ : Nontrivial R
h : (of R M) m ∈ Submodule.span R ↑(Submonoid.map (of R M) (Submonoid.closure s))
⊢ m ∈ Submonoid.closure s
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ ![x, y] 0 ≠ 0

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ (∑ a ∈ f.coeff.support, single a (f.coeff a)) • v ∈ ↑W

Tactic:
Finset.sum_smul

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ ∑ i ∈ f.coeff.support, single i (f.coeff i) • v ∈ ↑W
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
⊢ s ⊆ ↑(span K ↑ht.toFinset)

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ this.toFinset.card ≤ ht.toFinset.card

Tactic:
← Eq

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ this.toFinset.card ≤ u.card
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝³ : Semiring R
x✝ y✝ : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Subsingleton M
x y : R[M]
this : Unique M := { default := 1, uniq := ⋯ }
⊢ (x.coeff.sum fun m₁ r₁ ↦ y.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = 1 then r₁ * r₂ else 0) =
    (coeffAddEquiv.trans (uniqueAddEquiv 1)).toFun x * (coeffAddEquiv.trans (uniqueAddEquiv 1)).toFun y

Tactic:
simp [Finsupp.sum_unique, Unique.eq_default]

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

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
x✝ : UniqueMul A B a0 b0
⊢ ∀ (y : G × G), (fun ab ↦ ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0) y → y = (a0, b0)

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n) * #s ≤ #s ^ n * #s

Tactic:
by gcongr; exact card_pow_le

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ 1 ∈ t⁻¹

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑t
b : α
hb : b ∈ ↑t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ c * a ≠ c * b

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ a * c ≠ b * c

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
hs : s.Nontrivial
x✝ : 1 ≠ 0
⊢ (s ^ 1).Nontrivial

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i
s : Finset (Subtype (Membership.mem S))
hs : m ∈ ⨆ i ∈ s, ↑i
this : m ∈ ⨆ i, ⨆ (hi : i ∈ S), ⨆ (_ : ⟨i, hi⟩ ∈ s), i
⊢ m ∈ ⨆ i ∈ Finset.map (Function.Embedding.subtype fun x ↦ x ∈ S) s, i

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice β
a : α × β
⊢ a ∈ ⊤.prod L ↔ a ∈ comap LatticeHom.snd L

Tactic:
by simp [mem_prod, LatticeHom.coe_snd]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
hx : x ∈ p
⊢ x = ↑⟨x, hx⟩

Tactic:
Subtype.coe_mk

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
hx : x ∈ p
⊢ x = x
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.left.h_zero
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ ∀ (b : M), 0 • id b = 0

Tactic:
exact zero_smul _

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.right.h_zero
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ ∀ (b : M), 0 • id b = 0

Tactic:
exact zero_smul _

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
E : Type u_7
inst✝¹ : AddCommGroup E
inst✝ : Module S E
p : E →ₗ[S] E
hp : IsIdempotentElem p
⊢ p.ker = (id - p).range

Tactic:
by
  simpa using! hp.one_sub.range_eq_ker_one_sub.symm

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝¹ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R✝ R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
R : ι → SetRel α α
inst✝ : ∀ (i : ι), (R i).IsRefl
⊢ ∀ (R_1 : SetRel α α), (R_1 ∈ Set.range fun i ↦ R i) → R_1.IsRefl

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
inst✝ : R.IsSymm
⊢ R.inv.IsSymm

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝¹ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R✝ R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
R : ι → SetRel α α
inst✝ : ∀ (i : ι), (R i).IsSymm
⊢ ∀ (R_1 : SetRel α α), (R_1 ∈ Set.range fun i ↦ R i) → R_1.IsSymm

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝¹ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R✝ R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
R : ι → SetRel α α
inst✝ : ∀ (i : ι), (R i).IsTrans
⊢ ∀ (R_1 : SetRel α α), (R_1 ∈ Set.range fun i ↦ R i) → R_1.IsTrans

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
| 1 + ↑i

Tactic:
add_comm

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
| ↑i + 1
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q w : RelSeries r
hpq : (p.last, q.head) ∈ r
hqw : (q.last, w.head) ∈ r
⊢ ((p.append q hpq).last, w.head) ∈ r

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q w : RelSeries r
hpq : (p.last, q.head) ∈ r
hqw : (q.last, w.head) ∈ r
⊢ (p.last, (q.append w hqw).head) ∈ r

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last, q.head) ∈ r
hqw : (q.last, w.head) ∈ r
⊢ (p.append q hpq).append w ⋯ = p.append (q.append w hqw) ⋯

Tactic:
ext
  · simp only [append_length, Nat.add_left_inj]
    lia
  · simp [append, Fin.append_assoc]

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

Goal state before:
pp: R✝ : Type u
S✝ : Type u₁
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : Monoid R
inst✝⁹ : Monoid S
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : MulAction R S
inst✝⁵ : DistribMulAction S A
inst✝⁴ : DistribMulAction S B
inst✝³ : DistribMulAction R A
inst✝² : DistribMulAction R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₙₐ[S] B
r : R
x : A
this : f ((r • 1) • x) = (r • 1) • f x
⊢ (↑f).toFun (r • x) = (MonoidHom.id R) r • (↑f).toFun x

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) l
x : α
hx : (x, l.head l_ne_nil) ∈ r
⊢ (x, (fromListIsChain l l_ne_nil hl).head) ∈ r

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
x : α
hx : (x, p.head) ∈ r
hq : (p.last, q.head) ∈ r
⊢ ((p.cons x hx).last, q.head) ∈ r

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
x : α
hx : (x, p.head) ∈ r
hq : (p.last, q.head) ∈ r
⊢ (x, (p.append q hq).head) ∈ r

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap g r.mkQ.ker = f.range ⊔ q.mkQ.ker ↔ g.range ⊓ r ≤ map g q

Tactic:
ker_mkQ,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap g r = f.range ⊔ q.mkQ.ker ↔ g.range ⊓ r ≤ map g q
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap g r = f.range ⊔ q.mkQ.ker ↔ g.range ⊓ r ≤ map g q

Tactic:
ker_mkQ,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap g r = f.range ⊔ q ↔ g.range ⊓ r ≤ map g q
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hhead : x ≤ RelSeries.head p
⊢ (RelSeries.reverse p).last ≤ x

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
⊢ RelSeries.last p' = (RelSeries.drop p i).head

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = coheight (RelSeries.head p)
i : Fin (p.length + 1)
⊢ ↑(RelSeries.reverse p).length = height (RelSeries.reverse p).last

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = coheight (RelSeries.head p)
i : Fin (p.length + 1)
⊢ coheight (p.toFun i) = ↑↑i.rev

Tactic:
simpa using! height_eq_index_of_length_eq_height_last (α := αᵒᵈ) (p := p.reverse) (by simpa) i.rev

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
p : RelSeries {(a, b) | a < b}
x : β
hx : (x, p.head) ∈ {(a, b) | a < b}
ih : ∀ (a : α), p.head = f a → ↑p.length ≤ coheight a
a : α
hp : (p.cons x hx).head = f a
⊢ ↑(p.cons x hx).length ≤ coheight a

Tactic:
simp only [RelSeries.head_cons] at hp

Goal state after:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
p : RelSeries {(a, b) | a < b}
x : β
hx : (x, p.head) ∈ {(a, b) | a < b}
ih : ∀ (a : α), p.head = f a → ↑p.length ≤ coheight a
a : α
hp : x = f a
⊢ ↑(p.cons x hx).length ≤ coheight a
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ coheight a
p : LTSeries αᵒᵈ
hp : RelSeries.last p = a
hl : p.length = n
⊢ (RelSeries.reverse p).head = a

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ coheight a
p : LTSeries αᵒᵈ
hp : RelSeries.last p = a
hl : p.length = n
⊢ (RelSeries.reverse p).length = n

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries α
hp : RelSeries.head p = x
hl : p.length = n
⊢ (RelSeries.reverse p).last = x

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries α
hp : RelSeries.head p = x
hl : p.length = n
⊢ (RelSeries.reverse p).length = n

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ (RelSeries.reverse p).head = x

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ (RelSeries.reverse p).length = n

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
⊢ (![x, y] (Fin.castSucc 0), ![x, y] (Fin.succ 0)) ∈ {(a, b) | a < b}

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case «0»
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ (![y, x, z] ((fun i ↦ i) ⟨0, ⋯⟩).castSucc, ![y, x, z] ((fun i ↦ i) ⟨0, ⋯⟩).succ) ∈ {(a, b) | a < b}

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case «1»
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ (![y, x, z] ((fun i ↦ i) ⟨1, ⋯⟩).castSucc, ![y, x, z] ((fun i ↦ i) ⟨1, ⋯⟩).succ) ∈ {(a, b) | a < b}

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.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
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
r : R'
x✝ y✝ : FreeAddMonoid (M × N)
hxy : Eqv R M N x✝ y✝
x y : FreeAddMonoid (M × N)
⊢ (SMul.aux r) x + (SMul.aux r) y = (SMul.aux r) y + (SMul.aux r) x

Tactic:
add_comm

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁴ : CommSemiring R
inst✝³³ : CommSemiring R₂
inst✝³² : CommSemiring R₃
inst✝³¹ : Monoid R'
inst✝³⁰ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝²⁹ : AddCommMonoid M
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid P
inst✝²⁶ : AddCommMonoid Q
inst✝²⁵ : AddCommMonoid S
inst✝²⁴ : AddCommMonoid P'
inst✝²³ : AddCommMonoid Q'
inst✝²² : AddCommMonoid M₂
inst✝²¹ : AddCommMonoid N₂
inst✝²⁰ : AddCommMonoid P₂
inst✝¹⁹ : AddCommMonoid Q₂
inst✝¹⁸ : AddCommMonoid M₃
inst✝¹⁷ : AddCommMonoid N₃
inst✝¹⁶ : AddCommMonoid P₃
inst✝¹⁵ : AddCommMonoid Q₃
inst✝¹⁴ : DistribMulAction R' M
inst✝¹³ : Module R'' M
inst✝¹² : Module R M
inst✝¹¹ : Module R N
inst✝¹⁰ : Module R S
inst✝⁹ : Module R P'
inst✝⁸ : Module R Q'
inst✝⁷ : Module R₂ M₂
inst✝⁶ : Module R₂ N₂
inst✝⁵ : Module R₂ P₂
inst✝⁴ : Module R₂ Q₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₃ N₃
inst✝¹ : Module R₃ P₃
inst✝ : Module R₃ Q₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x✝ y✝ : FreeAddMonoid (M × N)
hxy : Eqv R M N x✝ y✝
x y : FreeAddMonoid (M × N)
⊢ (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) x + (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) y =
    (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) y + (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) x

Tactic:
add_comm

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = 0

Tactic:
← this

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = -x + x + (-y + y)