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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n✝ n : ℕ
⊢ mulRight R a ^ n * mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a

Tactic:
Module.End.mul_eq_comp,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n✝ n : ℕ
⊢ (mulRight R a ^ n) ∘ₗ mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
h : (Algebra.lmul R A) a₁ = (Algebra.lmul R A) a₂
⊢ a₁ = a₂

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
h : (Algebra.lmul R A) a₁ = (Algebra.lmul R A) a₂
⊢ a₁ = a₂
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
n : ℕ
h' : height (f x) = ↑n
⊢ height x ≤ (↑m + 1) * ↑n + ↑m

Tactic:
| coe n =>

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
e : α ↪o β
this : ∀ (b : β), Subsingleton ↑(⇑e ⁻¹' {b})
⊢ krullDim α ≤ krullDim β

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
e : α ↪o β
this : ∀ (b : β), Subsingleton ↑(⇑e ⁻¹' {b})
⊢ krullDim α ≤ krullDim β
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : FunLike F α β
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : F
⊢ ∀ (a : List (Set α)), ⇑f '' Multiset.prod ⟦a⟧ = (Multiset.map (fun s ↦ ⇑f '' s) ⟦a⟧).prod

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : FunLike F α β
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : F
⊢ ∀ (a : List (Set α)), ⇑f '' a.prod = (List.map (fun s ↦ ⇑f '' s) a).prod
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: α : Type u_2
inst✝ : CommMonoid α
n : ℕ
s : Set α
a : α
⊢ a ∈ s ^ n ↔ ∃ f, (∀ (i : Fin n), f i ∈ s) ∧ ∏ i, f i = a

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : CommMonoid α
n : ℕ
s : Set α
a : α
⊢ a ∈ s ^ n ↔ ∃ f, (∀ (i : Fin n), f i ∈ s) ∧ ∏ i, f i = a
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case refine_3
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
t : M ⊗[R] N
⊢ ∀ (x y : M ⊗[R] N),
    x ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} →
      y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → x + y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
· intro t₁ t₂ ht₁ ht₂
    exact Submodule.add_mem _ ht₁ ht₂

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Fintype ι
S : ι → Set α
⊢ (fun f ↦ ∏ i, f i) '' univ.pi S = ∏ i, S i

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Fintype ι
S : ι → Set α
⊢ (fun f ↦ ∏ i, f i) '' univ.pi S = ∏ i, S i
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f : N →ₗ[R] P
m : N
n : M
⊢ (((TensorProduct.mk R N M).compr₂ₛₗ (rTensor M (g ∘ₗ f))) m) n =
    (((TensorProduct.mk R N M).compr₂ₛₗ (rTensor M g ∘ₗ rTensor M f)) m) n

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, comp_apply, rTensor_tmul]

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

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a b : α
hb : 1 ≤ b
⊢ b * a ≤ b → a∗ ≤ b
Module: Mathlib.Algebra.Order.Kleene

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

Tactic:
simpa using mul_kstar_le hb

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:
simpa using

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a b : α
hb : 1 ≤ b
⊢ a * b ≤ b → a∗ ≤ b
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
⊢ b ∈ comap (AddMonoidHom.mulLeft a') (closure (S * T))

Tactic:
refine (closure_le.2 fun b' hb' => ?_) hb

Goal state after:
case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
⊢ b' ∈ ↑(comap (AddMonoidHom.mulLeft a') (closure (S * T)))
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ m * p + n * p ∈ M * P ⊔ N * P

Tactic:
exact add_mem_sup (mul_mem_mul hm hp) <| mul_mem_mul hn hp

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

Goal state before:
pp: case intro
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x ≤ f x₀

Tactic:
simpa using

Goal state after:
case intro
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x ≤ f x₀
Module: Mathlib.Data.Fintype.Lattice

Goal state before:
pp: case intro
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x

Tactic:
simpa using

Goal state after:
case intro
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: case h₂
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (b * y)

Tactic:
rw [mul_comm b, ← mul_assoc]
    exact (mul_dvd_mul_right H1 _).mul_right _

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
a b : R
H : a * (x + y * z) + b * y = 1
⊢ a * x + (a * z + b) * y = 1

Tactic:
simpa using

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (z * y + x) y
⊢ IsCoprime x y

Tactic:
rw [add_comm] at h
  exact h.of_add_mul_right_left

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z + y * -z) y

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : R
h : 2 ∣ x
⊢ IsCoprime (x + 1) (x - 1)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
x : R
h : 2 ∣ x
⊢ IsCoprime (x + 1) (x - 1)
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime (x + y * z + y * -z) y

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime x y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
h : 2 ∣ x
⊢ IsRelPrime (x + 1) (x - 1)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
h : 2 ∣ x
⊢ IsRelPrime (x + 1) (x - 1)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case mp
m n : ℤ
⊢ IsCoprime m n → m.gcd n = 1

pp: case mpr
m n : ℤ
⊢ m.gcd n = 1 → IsCoprime m n

Tactic:
· rintro ⟨a, b, h⟩
    refine Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, ?_⟩)
    rwa [mul_comm m, mul_comm n, eq_comm]

Goal state after:
case mpr
m n : ℤ
⊢ m.gcd n = 1 → IsCoprime m n
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: A : Type u
inst✝¹ : CommRing A
inst✝ : Nontrivial A
a b : ℕ
h : a.Coprime b
⊢ IsCoprime ↑a ↑b

Tactic:
simpa using

Goal state after:
A : Type u
inst✝¹ : CommRing A
inst✝ : Nontrivial A
a b : ℕ
h : a.Coprime b
⊢ IsCoprime ↑a ↑b
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ (∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (∏ i ∈ t, s i)

Tactic:
simpa using

Goal state after:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ (∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (∏ i ∈ t, s i)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ IsCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsCoprime x (s i)

Tactic:
simpa using

Goal state after:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ IsCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsCoprime x (s i)
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : 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 j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
a b c : α
⊢ decide (a ≤ b) = true → decide (b ≤ c) = true → decide (a ≤ c) = true

Tactic:
simpa using

Goal state after:
α : 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 j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
a b c : α
⊢ a ≤ b → b ≤ c → a ≤ c
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : 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 j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
⊢ ∀ (a b : α), (decide (a ≤ b) || decide (b ≤ a)) = true

Tactic:
simpa using

Goal state after:
α : 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 j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
⊢ ∀ (a b : α), a ≤ b ∨ b ≤ a
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : 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 j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hj.choose < ↑hi.choose
⊢ sli[↑hj.choose] ≤ sli[↑hi.choose]

Tactic:
simpa using

Goal state after:
α : 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 j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hj.choose < ↑hi.choose
⊢ sli[↑hj.choose] ≤ sli[↑hi.choose]
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case neg.refine_2
α : 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 j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hi.choose ≤ ↑hj.choose
⊢ sli[↑hi.choose] ≤ sli[↑hj.choose]

Tactic:
simpa using

Goal state after:
case neg.refine_2
α : 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 j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hi.choose ≤ ↑hj.choose
⊢ sli[↑hi.choose] ≤ sli[↑hj.choose]
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val i < toInt val j ↔ val i < val j

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val i < toInt val j ↔ val i < val j
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val i ≠ toInt val j ↔ val i ≠ val j

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ ¬toInt val i = toInt val j ↔ ¬val i = val j
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ ¬toInt val i ≤ toInt val j ↔ ¬val i ≤ val j

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val j < toInt val i ↔ val j < val i
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ ¬toInt val i < toInt val j ↔ ¬val i < val j

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val j ≤ toInt val i ↔ val j ≤ val i
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α✝ : Type u_1
inst✝ : LinearOrder α✝
n : ℕ
val : Fin n → α✝
i j k : Fin n
u : Level
α :
  let u := u;
  Q(Type u)
atoms : Array Q(«$α»)
h : ¬atoms.isEmpty = true
⊢ 0 < atoms.size

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
inst✝ : LinearOrder α✝
n : ℕ
val : Fin n → α✝
i j k : Fin n
u : Level
α :
  let u := u;
  Q(Type u)
atoms : Array Q(«$α»)
h : ¬atoms.isEmpty = true
⊢ ¬atoms = #[]
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
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ p x hx

Tactic:
by
  refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H
  exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩)
    fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩

Goal state after:
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
P : Submodule R A
x y : A
⊢ x ∈ P * (R ∙ y) ↔ ∃ z ∈ P, z * y = x

Tactic:
by
  simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map_flip, mem_map, LinearMap.flip_apply,
    LinearMap.mul_apply_apply]

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 x (s i)) → IsRelPrime x (∏ i ∈ t, s i)

Tactic:
simpa using

Goal state after:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ (∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i)
Module: Mathlib.RingTheory.Coprime.Lemmas

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

Tactic:
simpa using

Goal state after:
α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ IsRelPrime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsRelPrime x (s i)
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
inst✝ : FaithfulSMul R A
x✝ : Aˣ
⊢ x✝ ∈ (Units.map ↑(spanSingleton R)).ker ↔ x✝ ∈ (Units.map ↑(algebraMap R A)).range

Tactic:
simpa using

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : Aˣ
⊢ 1 = R ∙ ↑x✝ ↔ ∃ x, ↑x✝ = (algebraMap R A) ↑x
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s' : S
h₁ : (r, s') ∈ I
r' : R
s : S
h₂ : (r', s) ∈ I
⊢ ((RingHom.fst R S) (r, s'), (RingHom.snd R S) (r', s)) ∈ I

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s' : S
h₁ : (r, s') ∈ I
r' : R
s : S
h₂ : (r', s) ∈ I
⊢ (r, s) ∈ I
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
hI : I ≤ 1
⊢ I ≤ I * (1 / I)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
hI : I ≤ 1
⊢ I ≤ I * (1 / I)
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
this : (x, 1) * (y, 1) ∈ I.prod ⊤
⊢ x ∈ I ∨ y ∈ I

Tactic:
simpa using

Goal state after:
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
this : (x, 1) * (y, 1) ∈ I.prod ⊤
⊢ x ∈ I ∨ y ∈ I
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
⊢ I.prod ⊤ ≠ ⊤

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
⊢ ¬I = ⊤
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
x y : R × S
⊢ x * y ∈ I.prod ⊤ → x ∈ I.prod ⊤ ∨ y ∈ I.prod ⊤

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
x y : R × S
⊢ x.1 * y.1 ∈ I → x.1 ∈ I ∨ y.1 ∈ I
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal I

Tactic:
I.ideal_prod_eq,

Goal state after:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal ((Ideal.map (RingHom.fst R S) I).prod (Ideal.map (RingHom.snd R S) I))
Module: Mathlib.RingTheory.OrzechProperty

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
⊢ Injective ⇑i'

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
⊢ Injective ⇑i
Module: Mathlib.RingTheory.OrzechProperty

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
f' : ↥i'.range →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ f ∘ₗ ↑(LinearEquiv.ofInjective i' hi).symm
⊢ Surjective ⇑f'

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
f' : ↥i'.range →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ f ∘ₗ ↑(LinearEquiv.ofInjective i' hi).symm
⊢ Surjective ⇑f