mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0

Tactic:
rcases hc with hc | hc

Goal state after:
case inl
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
hc : 1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0

case inr
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inr.intro.intro.left
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ UniqueMul A B p1.1 p1.2

Tactic:
refine UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans hc')

Goal state after:
case inr.intro.intro.left.refine_1
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ f p1.1 ∈ image (⇑f) A

case inr.intro.intro.left.refine_2
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ f p1.2 ∈ image (⇑f) B
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inr.intro.intro.right
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ UniqueMul A B p2.1 p2.2

Tactic:
refine UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans hc')

Goal state after:
case inr.intro.intro.right.refine_1
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ f p2.1 ∈ image (⇑f) A

case inr.intro.intro.right.refine_2
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ f p2.2 ∈ image (⇑f) B
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 q : Submodule R E
h : IsCompl p q
x : E
⊢ (q.projection p ⋯) x ∈ q

Tactic:
exact projection_apply_mem h.symm x

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

Goal state before:
pp: M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst✝ : One P
hg : 1 ∈ Set.range g
⊢ MulExact f g ↔ MulExact Subtype.val (Set.rangeFactorization g)

Tactic:
let : One (Set.range g) := ⟨⟨1, hg⟩⟩

Goal state after:
M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst✝ : One P
hg : 1 ∈ Set.range g
this : One ↑(Set.range g) := { one := ⟨1, hg⟩ }
⊢ MulExact f g ↔ MulExact Subtype.val (Set.rangeFactorization g)
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ (⨅ i, ↑(f i)).toNat = ⨅ i, f i

Tactic:
norm_cast

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
⊢ IsProj f.range f ↔ IsIdempotentElem f

Tactic:
refine ⟨fun ⟨h1, h2⟩ => ?_, fun hf =>
    ⟨fun x => mem_range_self f x, fun x ⟨y, hy⟩ => by rw [← hy, ← Module.End.mul_apply, hf.eq]⟩⟩

Goal state after:
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
x✝ : IsProj f.range f
h1 : ∀ (x : M), f x ∈ f.range
h2 : ∀ x ∈ f.range, f x = x
⊢ IsIdempotentElem f
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N ≃ₗ[R] N'
⊢ Submodule.map (↑e) g.ker = Submodule.map (↑e) f.range ↔ g.ker = f.range

Tactic:
exact (Submodule.map_injective_of_injective e.injective).eq_iff

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid N'
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid P'
inst✝⁵ : Module R M
inst✝⁴ : Module R M'
inst✝³ : Module R N
inst✝² : Module R N'
inst✝¹ : Module R P
inst✝ : Module R P'
f₁₂ : M →ₗ[R] N
f₂₃ : N →ₗ[R] P
g₁₂ : M' →ₗ[R] N'
g₂₃ : N' →ₗ[R] P'
e₁ : M ≃ₗ[R] M'
e₂ : N ≃ₗ[R] N'
e₃ : P ≃ₗ[R] P'
h₁₂ : g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂
h₂₃ : g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃
H : Exact ⇑f₁₂ ⇑f₂₃
⊢ Exact ⇑g₁₂ ⇑g₂₃

Tactic:
iff_of_ladder_linearEquiv h₁₂ h₂₃

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid N'
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid P'
inst✝⁵ : Module R M
inst✝⁴ : Module R M'
inst✝³ : Module R N
inst✝² : Module R N'
inst✝¹ : Module R P
inst✝ : Module R P'
f₁₂ : M →ₗ[R] N
f₂₃ : N →ₗ[R] P
g₁₂ : M' →ₗ[R] N'
g₂₃ : N' →ₗ[R] P'
e₁ : M ≃ₗ[R] M'
e₂ : N ≃ₗ[R] N'
e₃ : P ≃ₗ[R] P'
h₁₂ : g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂
h₂₃ : g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃
H : Exact ⇑f₁₂ ⇑f₂₃
⊢ Exact ⇑f₁₂ ⇑f₂₃
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
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.ker ∈ Module.End.invtSubmodule T ↔ f.ker ≤ (f ∘ₗ T).ker

Tactic:
ker_comp,

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.ker ∈ Module.End.invtSubmodule T ↔ f.ker ≤ comap T f.ker
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ ∀ (i : ℕ) (_hi : i < x.length), (x.toList[i], x.toList[i + 1]) ∈ r

Tactic:
intro i

Goal state after:
α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
⊢ ∀ (_hi : i < x.length), (x.toList[i], x.toList[i + 1]) ∈ r
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case h
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ ∀ (i : ℕ) (h₁ : i < (p.append q connect).toList.length) (h₂ : i < (p.toList ++ q.toList).length),
    (p.append q connect).toList[i] = (p.toList ++ q.toList)[i]

Tactic:
· simp [List.getElem_append, Fin.append, Fin.addCases]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M
y : N
⊢ (LinearMap.fst R M N) (x, y) = 0 ↔ (x, y) ∈ Set.range ⇑(LinearMap.inr R M N)

Tactic:
simp only [LinearMap.fst_apply, @eq_comm _ x, LinearMap.coe_inr, Set.mem_range, Prod.mk.injEq,
    exists_eq_right]

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
⊢ (r.mkQ ∘ₗ g).ker = comap q.mkQ (q.mkQ ∘ₗ f).range ↔ g.range ⊓ r ≤ map g q

Tactic:
ker_comp,

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.mkQ.ker = comap q.mkQ (q.mkQ ∘ₗ f).range ↔ g.range ⊓ r ≤ map g q
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case h
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ ∀ (i : ℕ) (h₁ : i < p.eraseLast.toList.length) (h₂ : i < p.toList.dropLast.length),
    p.eraseLast.toList[i] = p.toList.dropLast[i]

Tactic:
intro i

Goal state after:
case h
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
i : ℕ
⊢ ∀ (h₁ : i < p.eraseLast.toList.length) (h₂ : i < p.toList.dropLast.length),
    p.eraseLast.toList[i] = p.toList.dropLast[i]
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.eraseLast.snoc p.last ⋯ = p

Tactic:
apply toList_injective
  rw [toList_snoc, ← getLast_toList, toList_eraseLast _ h, List.dropLast_append_getLast]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case left
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
⊢ ∀ (i : Fin p.length),
    (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd q.length i).castSucc,
        Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd q.length i).succ) ∈
      r

Tactic:
intro i

Goal state after:
case left
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd q.length i).castSucc,
      Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd q.length i).succ) ∈
    r
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case right
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
⊢ ∀ (i : Fin q.length),
    (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i).castSucc,
        Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i).succ) ∈
      r

Tactic:
intro i

Goal state after:
case right
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin q.length
⊢ (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i).castSucc,
      Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i).succ) ∈
    r
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p.length - 1 + 1 ≤ height x
⊢ ↑p.length = ↑p.length - 1 + 1

Tactic:
norm_cast

Goal state after:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p.length - 1 + 1 ≤ height x
⊢ p.length = p.length - 1 + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last < x

Tactic:
rw [← hp]

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last < RelSeries.last p
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ height (RelSeries.eraseLast p).last + 1

Tactic:
height_add_const

Goal state after:
case a.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ⨆ p_1, ⨆ (_ : RelSeries.last p_1 = (RelSeries.eraseLast p).last), ↑p_1.length + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ height y + 1 ≤ height x

Tactic:
height_add_const

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = y), ↑p.length + 1 ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ ↑a✝ + 1 ≤ ↑n ↔ ↑a✝ < ↑n

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < x

Tactic:
rw [← hp]

Goal state after:
case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < RelSeries.last p
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_2.coe
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ a✝ ≤ n ↔ ↑a✝ < ↑n + 1

Tactic:
norm_cast

Goal state after:
case e'_2.coe
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ a✝ ≤ n ↔ a✝ < n + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
⊢ ↑(LTSeries.longestOf α).length ≤ ↑(⨆ p, ⨆ (_ : RelSeries.last p ≤ RelSeries.last (LTSeries.longestOf α)), ↑p.length)

Tactic:
norm_cast

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
⊢ ↑(LTSeries.longestOf α).length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ RelSeries.last (LTSeries.longestOf α)), ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x + 1 ≤ height ↑x

Tactic:
height_add_const

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = x), ↑p.length + 1 ≤ height ↑x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ y, ⨆ (_ : y < ⊤), height y + 1) = ↑(⨆ a, height a) + 1

Tactic:
norm_cast

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ y, ⨆ (_ : y < ⊤), height y + 1 = (⨆ a, height a) + 1
Module: Mathlib.Algebra.Order.Kleene

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

Tactic:
grw [hb, kstar_mul_le_self ha]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
⊢ -x * y = -(x * y)

Tactic:
refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_) <;>
        simp only [AddSubmonoid.mem_neg, ← neg_mul] at *
    · exact mul_mem_mul hm hn
    · exact mul_mem_mul (neg_mem_neg.2 hm) hn

Goal state after:
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y

Tactic:
rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y * a * x + b * (y * z)
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ z

Tactic:
rw [← one_mul z, ← H, add_mul, mul_right_comm, mul_assoc b]

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ a * z * x + b * (y * z)
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case h
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := ⋯
sli : List α := ⋯
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
⊢ ∀ (i j : Fin n), val i ≤ val j ↔ (fun i ↦ ↑↑⋯.choose) i ≤ (fun i ↦ ↑↑⋯.choose) j

Tactic:
intro i

Goal state after:
case h
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
i : Fin n
⊢ ∀ (j : Fin n), val i ≤ val j ↔ (fun i ↦ ↑↑⋯.choose) i ≤ (fun i ↦ ↑↑⋯.choose) j
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ span R s ^ 0 = span R (s ^ 0)

Tactic:
by rw [pow_zero, pow_zero, one_eq_span_one_set]

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x

Tactic:
classical
  refine Finset.induction_on t (fun _ ↦ isRelPrime_one_left) fun b t hbt ih H ↦ ?_
  rw [Finset.prod_insert hbt]
  rw [Finset.forall_mem_insert] at H
  exact H.1.mul_left (ih H.2)

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
⊢ Pairwise (IsRelPrime on fun i ↦ s ↑i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)

Tactic:
by
  refine ⟨fun hp i hi ↦ IsRelPrime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
  · rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
    obtain ⟨hj, ji⟩ := hj
    exact @hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm
  · rintro ⟨i, hi⟩ ⟨j, hj⟩ h
    apply IsRelPrime.prod_right_iff.mp (hp i hi)
    grind

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
H : IsRelPrime x y
⊢ IsRelPrime (x ^ m) y

Tactic:
by
  rw [← Finset.card_range m, ← Finset.prod_const]
  exact IsRelPrime.prod_left fun _ _ ↦ H

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

Goal state before:
pp: case refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ restrictScalars S (⇑(algebraMap S R) '' s • N)
⊢ x ∈ s • restrictScalars S N

Tactic:
rw [restrictScalars_mem] at x_in
    refine set_smul_inductionOn x x_in ?_ ?_ (fun _ _ _ _ h h' ↦ add_mem h h') (zero_mem _)
    · rintro _ x ⟨r, r_in, rfl⟩ x_in
      rw [algebraMap_smul]
      exact mem_set_smul_of_mem_mem r_in x_in
    · intro r y h h'
      obtain ⟨c, c_supp, hc⟩ := (mem_set_smul ..).mp <| smul_mem _ r h
      simp only [hc, Finsupp.sum, AddSubmonoidClass.coe_finsetSum, SetLike.val_smul]
      refine sum_mem fun u u_in ↦ ?_
      obtain ⟨u, u_in', rfl⟩ := c_supp (Finset.mem_coe.mpr u_in)
      rw [algebraMap_smul]
      exact mem_set_smul_of_mem_mem u_in' (coe_mem (c ((algebraMap S R) u)))

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set (Ideal S)
⊢ ⨅ I ∈ s, comap f I = ⨅ I ∈ comap f '' s, I

Tactic:
iInf_image

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set (Ideal S)
⊢ ⨅ I ∈ s, comap f I = ⨅ b ∈ s, comap f b
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : Π₀ (i : ι), M i), r • m = 0
⊢ ∀ (i : ι) (m : M i), r • m = 0

Tactic:
intro i

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : Π₀ (i : ι), M i), r • m = 0
i : ι
⊢ ∀ (m : M i), r • m = 0