mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝⁴² : Semiring R
inst✝⁴¹ : Semiring R₂
inst✝⁴⁰ : Semiring S
inst✝³⁹ : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝³⁸ : AddCommMonoid M
inst✝³⁷ : AddCommMonoid M₂
inst✝³⁶ : AddCommMonoid N
inst✝³⁵ : AddCommMonoid N₂
inst✝³⁴ : AddCommMonoid P
inst✝³³ : AddCommMonoid P₂
inst✝³² : AddCommMonoid Pₗ
inst✝³¹ : Module R M
inst✝³⁰ : Module R M₂
inst✝²⁹ : Module S N
inst✝²⁸ : Module S N₂
inst✝²⁷ : Module R₂ P
inst✝²⁶ : Module S₂ P
inst✝²⁵ : Module R P₂
inst✝²⁴ : Module S₂ P₂
inst✝²³ : Module R Pₗ
inst✝²² : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝²¹ : AddCommGroup M'
inst✝²⁰ : AddCommGroup P'
inst✝¹⁹ : Module R M'
inst✝¹⁸ : Module R₂ P'
inst✝¹⁷ : Module S₂ P'
inst✝¹⁶ : SMulCommClass S₂ R₂ P
inst✝¹⁵ : SMulCommClass S R Pₗ
inst✝¹⁴ : SMulCommClass S₂ R₂ P'
inst✝¹³ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst✝¹² : Semiring R'
inst✝¹¹ : Semiring S'
inst✝¹⁰ : Module R' M
inst✝⁹ : Module S' N
inst✝⁸ : Module R' Pₗ
inst✝⁷ : Module S' Pₗ
inst✝⁶ : SMulCommClass S' R' Pₗ
inst✝⁵ : SMul S' S
inst✝⁴ : IsScalarTower S' S N
inst✝³ : IsScalarTower S' S Pₗ
inst✝² : SMul R' R
inst✝¹ : IsScalarTower R' R M
inst✝ : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x✝ : N
⊢ (B (r' • m)) x✝ = r' • (B m) x✝

Tactic:
← smul_one_smul R r' m,

Goal state after:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝⁴² : Semiring R
inst✝⁴¹ : Semiring R₂
inst✝⁴⁰ : Semiring S
inst✝³⁹ : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝³⁸ : AddCommMonoid M
inst✝³⁷ : AddCommMonoid M₂
inst✝³⁶ : AddCommMonoid N
inst✝³⁵ : AddCommMonoid N₂
inst✝³⁴ : AddCommMonoid P
inst✝³³ : AddCommMonoid P₂
inst✝³² : AddCommMonoid Pₗ
inst✝³¹ : Module R M
inst✝³⁰ : Module R M₂
inst✝²⁹ : Module S N
inst✝²⁸ : Module S N₂
inst✝²⁷ : Module R₂ P
inst✝²⁶ : Module S₂ P
inst✝²⁵ : Module R P₂
inst✝²⁴ : Module S₂ P₂
inst✝²³ : Module R Pₗ
inst✝²² : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝²¹ : AddCommGroup M'
inst✝²⁰ : AddCommGroup P'
inst✝¹⁹ : Module R M'
inst✝¹⁸ : Module R₂ P'
inst✝¹⁷ : Module S₂ P'
inst✝¹⁶ : SMulCommClass S₂ R₂ P
inst✝¹⁵ : SMulCommClass S R Pₗ
inst✝¹⁴ : SMulCommClass S₂ R₂ P'
inst✝¹³ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst✝¹² : Semiring R'
inst✝¹¹ : Semiring S'
inst✝¹⁰ : Module R' M
inst✝⁹ : Module S' N
inst✝⁸ : Module R' Pₗ
inst✝⁷ : Module S' Pₗ
inst✝⁶ : SMulCommClass S' R' Pₗ
inst✝⁵ : SMul S' S
inst✝⁴ : IsScalarTower S' S N
inst✝³ : IsScalarTower S' S Pₗ
inst✝² : SMul R' R
inst✝¹ : IsScalarTower R' R M
inst✝ : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x✝ : N
⊢ (B ((r' • 1) • m)) x✝ = r' • (B m) x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ LinearIndependent R v ↔ ((LinearMap.lsum R (fun x ↦ R) ℕ) fun i ↦ LinearMap.id.smulRight (v i)).ker = ⊥

Tactic:
simp [Fintype.linearIndependent_iff, LinearMap.ker_eq_bot', funext_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
this : ((lsum ℕ) fun i ↦ (p i).subtype).ker = ⊥
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)

Tactic:
rw [LinearMap.ker_eq_bot] at this

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
this : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ s = 0

Tactic:
suffices (a * d) • s = (b * c) • s by
      by_contra hs; exact h (_root_.smul_left_injective S hs ‹_›)

Goal state after:
case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ (a * d) • s = (b * c) • s
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
⊢ ∃ s t, s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ (s = 0 → t ≠ 0)

Tactic:
by_cases hbd : b = 0 ∧ d = 0

Goal state after:
case pos
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
⊢ ∃ s t, s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ (s = 0 → t ≠ 0)

case neg
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : ¬(b = 0 ∧ d = 0)
⊢ ∃ s t, s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ (s = 0 → t ≠ 0)
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
a : FreeAbelianGroup X
⊢ a = ∑ x ∈ a.support, (coeff x) a • of x

Tactic:
conv_lhs => rw [← toFreeAbelianGroup_toFinsupp a, ← sum_single a.toFinsupp]

Goal state after:
X : Type u_1
a : FreeAbelianGroup X
⊢ toFreeAbelianGroup ((toFinsupp a).sum single) = ∑ x ∈ a.support, (coeff x) a • of x
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
b : α
hb : b ∈ s
h : ¬Disjoint (image (f a) t) (image (f b) t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)

Tactic:
union_eq_right.2

Goal state after:
case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
b : α
hb : b ∈ s
h : ¬Disjoint (image (f a) t) (image (f b) t)
⊢ #t ∣ #(image₂ f s t)

case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
b : α
hb : b ∈ s
h : ¬Disjoint (image (f a) t) (image (f b) t)
⊢ image (fun b ↦ f a b) t ⊆ image₂ f s t
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g = t.sup' ⋯ fun y ↦ s.sup' ⋯ fun x ↦ g (f x y)

Tactic:
by
  simp only [image₂, sup'_image, sup'_product_right]; rfl

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 ⊆ ↑u

Tactic:
by simp [hsu]

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

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Tactic:
obtain ⟨ha, hb⟩ := Finset.mem_product.mp hab

Goal state after:
G : Type u_1
inst✝ : Mul G
A B : Finset G
x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
ha : (a, b).1 ∈ A
hb : (a, b).2 ∈ B
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ k ≤ #(image f univ)

Tactic:
card_image_of_injective _ hmono.injective,

Goal state after:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ k ≤ #univ
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
a : R[ℕ]
n : ℕ
n_ih : { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := a ^ (n + 1) } = npowRec (n + 1) { toFinsupp := a }

Tactic:
simp [npowRec, n_ih, pow_succ]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a n : ℕ
h : a.AtLeastTwo
⊢ (OfNat.ofNat a).coeff (n + 1) = 0

Tactic:
rw [← Nat.cast_ofNat]
  simp [-Nat.cast_ofNat]

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

Goal state before:
pp: case left
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 : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ (fun y ↦ if H : y ∈ t1 then g y H else 0) y ∈ s

Tactic:
simp only [dif_pos H]
      apply hg1

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

Goal state before:
pp: case right
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 : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ f ((fun y ↦ if H : y ∈ t1 then g y H else 0) y) = y

Tactic:
simp only [dif_pos H]
      apply hg2

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

Goal state before:
pp: case a.refine_1
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
⊢ (lmapDomain R R g) l ∈ supported R R (g '' ↑t1)

Tactic:
have : Inhabited P := ⟨0⟩

Goal state after:
case a.refine_1
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
this : Inhabited P
⊢ (lmapDomain R R g) l ∈ supported R R (g '' ↑t1)
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑T ↔ Commute f ↑T ∧ Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm

Tactic:
iff_self_and

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑T → Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
M₂ : Type u_5
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₂ →ₗ[R] N →ₗ[R] P
g : M →ₗ[R] M₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.flip.compl₂ g) q p = map₂ (f ∘ₗ g) p q

Tactic:
← map₂_flip

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
M₂ : Type u_5
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₂ →ₗ[R] N →ₗ[R] P
g : M →ₗ[R] M₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.flip.compl₂ g).flip p q = map₂ (f ∘ₗ g) p q
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderBot α
h : ⊥ < x
⊢ 0 < height x

Tactic:
rw [height_pos]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderBot α
h : ⊥ < x
⊢ ¬IsMin x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderBot α
h : ⊥ < x
⊢ 0 < height x

Tactic:
by
  rw [height_pos]
  grind [not_isMin_iff]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case mp.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1) → α
hl : ∀ (i : Fin 0), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := 0, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

pp: case mp.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1 + 1) → α
hl : ∀ (i : Fin (0 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := 0 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

pp: case mp.succ.succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
l : Fin (n + 1 + 1 + 1) → α
hl : ∀ (i : Fin (n + 1 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := n + 1 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
· cases hl'.not_ge (by simp)

Goal state after:
case mp.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1 + 1) → α
hl : ∀ (i : Fin (0 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := 0 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

case mp.succ.succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
l : Fin (n + 1 + 1 + 1) → α
hl : ∀ (i : Fin (n + 1 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := n + 1 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case mp.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1 + 1) → α
hl : ∀ (i : Fin (0 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := 0 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

pp: case mp.succ.succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
l : Fin (n + 1 + 1 + 1) → α
hl : ∀ (i : Fin (n + 1 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := n + 1 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
· cases hl'.not_ge (by simp)

Goal state after:
case mp.succ.succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
l : Fin (n + 1 + 1 + 1) → α
hl : ∀ (i : Fin (n + 1 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := n + 1 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : IsEmpty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

pp: case inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : Nonempty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
· simp [krullDim_eq_bot]

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : Nonempty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

pp: case inr.inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
· rw [krullDim_eq_length_of_finiteDimensionalOrder, Nat.cast_le]
    constructor
    · exact fun H ↦ ⟨(LTSeries.longestOf α).take ⟨_, Nat.lt_succ_of_le H⟩, rfl⟩
    · exact fun ⟨l, hl⟩ ↦ hl ▸ l.longestOf_is_longest

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ krullDim α < ↑n ↔ ∀ (l : LTSeries α), l.length < n

Tactic:
rw [krullDim, ← WithBot.coe_natCast]

Goal state after:
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑n ↔ ∀ (l : LTSeries α), l.length < n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ↑(height a) ≤ krullDim α

Tactic:
by
  have : Nonempty α := ⟨a⟩
  rw [krullDim_eq_iSup_length]
  simp only [WithBot.coe_le_coe]
  exact height_le fun p _ ↦ le_iSup_of_le p le_rfl

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case refine_2
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.last = ⊤

Tactic:
rw [← h₂, RelSeries.last, RelSeries.last, ← hi₂, ← hit, Function.comp]

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

Goal state before:
pp: R : Type u_1
R' : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : Monoid R'
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : DistribMulAction R' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R' M
x : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
m : M
n : N
⊢ 1 • m ⊗ₜ[R] n = m ⊗ₜ[R] n

Tactic:
by rw [this, one_smul]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
r s : R
m : M
n : N
⊢ (r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n

Tactic:
by
  simp_rw [smul_tmul, tmul_smul, mul_smul]

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'₂ : Type u_22
inst✝³ : Monoid R'₂
inst✝² : DistribMulAction R'₂ M
inst✝¹ : SMulCommClass R R'₂ M
inst✝ : SMulCommClass R' R'₂ M
r' : R'
r'₂ : R'₂
x✝ x y : M ⊗[R] N
ihx : r' • r'₂ • x = r'₂ • r' • x
ihy : r' • r'₂ • y = r'₂ • r' • y
⊢ r' • r'₂ • (x + y) = r'₂ • r' • (x + y)

Tactic:
simp_rw [TensorProduct.smul_add]; rw [ihx, ihy]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_7
P : Type u_9
Q : Type u_10
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R M
inst✝¹ : Module R P
inst✝ : Module R Q
f : P →ₗ[R] Q →ₗ[R] M
p : Submodule R P
q : Submodule R Q
⊢ Submodule.map₂ f p q = (lift f ∘ₗ mapIncl p q).range

Tactic:
simp_rw [LinearMap.range_comp, range_mapIncl, Submodule.map_map₂]
  rfl

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a b : α
hb : 1 ≤ b
⊢ a * b ≤ b → a∗ ≤ b

Tactic:
by
  simpa using kstar_mul_le hb

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
⊢ a∗ ≤ 1 + a∗ * a

Tactic:
suffices 1 + (1 + a∗ * a) * a ≤ 1 + a∗ * a by
    rw [add_le_iff] at this
    nth_rw 1 [← one_mul a∗]
    exact (mul_left_mono this.1).trans (mul_kstar_le_self this.2)

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
⊢ 1 + (1 + a∗ * a) * a ≤ 1 + a∗ * a
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ lTensor M (f - g) = lTensor M f - lTensor M g

Tactic:
simp_rw [← coe_lTensorHom]
  exact (lTensorHom (R := R) (N := N) (P := P) M).map_sub f g

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
x✝ : A
⊢ x✝ ∈ toSubMulAction 1 ↔ x✝ ∈ 1

Tactic:
rw [one_eq_span, SubMulAction.mem_one]; exact mem_span_singleton

Goal state after: