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

Goal state before:
pp: case refine_1.left
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✝¹² : 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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring 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
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : N
e : ↑l x = ↑l y ∧ g x = g y
z : M
hz : f z = x - y
⊢ f (↑l (f z)) = 0

Tactic:
hz,

Goal state after:
case refine_1.left
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✝¹² : 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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring 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
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : N
e : ↑l x = ↑l y ∧ g x = g y
z : M
hz : f z = x - y
⊢ f (↑l (x - y)) = 0
Module: Mathlib.Algebra.Algebra.NonUnitalHom

Goal state before:
pp: R : Type u
S : Type u₁
T : Type u_1
inst✝¹⁰ : Monoid R
inst✝⁹ : Monoid S
inst✝⁸ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : DistribMulAction R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction S B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring B₁
inst✝ : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse ⇑φ' ⇑φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ g 0 = 0

Tactic:
rw [← f.map_zero, h₁]

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
⊢ (↑f).toFun (r • x) = (MonoidHom.id R) r • (↑f).toFun x

Tactic:
have := map_smul f (r • 1) x

Goal state after:
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
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
d : ℕ
hd : (p : RelSeries r) → p.length = d → motive p
p : RelSeries r
heq : p.length = d + 1
lq : (p.tail ⋯).length = p.length - 1
⊢ motive p

Tactic:
nth_rw 3 [heq] at lq

Goal state after:
case succ
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
d : ℕ
hd : (p : RelSeries r) → p.length = d → motive p
p : RelSeries r
heq : p.length = d + 1
lq : (p.tail ⋯).length = d + 1 - 1
⊢ motive p
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ (p.smash q h).toFun (Fin.natAdd p.length i).succ = q.toFun i.succ

Tactic:
dsimp only [smash, Fin.succ_natAdd]

Goal state after:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i.succ) = q.toFun i.succ
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
⊢ (p.smash q h).head = p.head

Tactic:
by
  obtain ⟨_ | _, _⟩ := p
  · simpa [Fin.addCases] using! h.symm
  dsimp only [smash, head]
  exact Fin.addCases_left 0

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.last (p.length + q.length)) = q.toFun (Fin.last q.length)

Tactic:
← Fin.natAdd_last,

Goal state after:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length (Fin.last q.length)) = q.toFun (Fin.last q.length)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ 0 < krullDim α ↔ krullDim α < 0 ∨ 0 < krullDim α

Tactic:
or_iff_right

Goal state after:
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ 0 < krullDim α ↔ 0 < krullDim α

α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ ¬krullDim α < 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ 0 < krullDim α ↔ krullDim α < 0 ∨ 0 < krullDim α

Tactic:
or_iff_right

Goal state after:
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ 0 < krullDim α ↔ 0 < krullDim α

α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ ¬krullDim α < 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ BddAbove (Set.range height)

Tactic:
bddDefault

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ BddAbove (Set.range fun a ↦ height a + coheight a)

Tactic:
bddDefault

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M ⊗[R] N →ₗ[R] P
⊢ lift ((mk R M N).compr₂ f) = f

Tactic:
rw [lift_compr₂ f, lift_mk, LinearMap.comp_id]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
x : α
⊢ coheight x < ⊤

Tactic:
by
  rw [← WithBot.coe_lt_coe]
  apply lt_of_le_of_lt (coheight_le_krullDim x)
  simpa using krullDim_ne_top_of_finiteDimensionalOrder.lt_top

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

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✝¹ : Module R P
inst✝ : Module R Q
g✝ : P →ₗ[R] Q
f✝ f g : N →ₗ[R] P
⊢ lTensor M (f + g) = lTensor M f + lTensor M g

Tactic:
ext x y
    simp only [compr₂ₛₗ_apply, mk_apply, add_apply, lTensor_tmul, tmul_add]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ a_1, ∃ z ∈ a, a_1 • z = x) → x ∈ a

Tactic:
rintro ⟨r, y, hy, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
r : R
y : M
hy : y ∈ a
⊢ r • y ∈ a
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
⊢ 1 * a = a

Tactic:
by
    ext x
    simp only [mem_mul, mem_one, smul_mul_assoc, exists_exists_eq_and, one_mul]
    refine ⟨?_, fun hx => ⟨1, x, hx, one_smul _ _⟩⟩
    rintro ⟨r, y, hy, rfl⟩
    exact smul_mem _ _ hy

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

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

Tactic:
exact IsCoprime.of_mul_left_left h

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
suffices IsCoprime m n by simpa [hn]

Goal state after:
case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case mpr
m n : ℤ
h : m.gcdA n * m + m.gcdB n * n = 1
⊢ ∃ a b, a * m + b * n = 1

Tactic:
exact ⟨_, _, h⟩

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := ⋯
sli : List α := ⋯
i : Fin n
⊢ val i ∈ sli

Tactic:
rw [List.Perm.mem_iff (List.mergeSort_perm _ _)]

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)
i : Fin n
⊢ val i ∈ li
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1
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
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ (LinearMap.toSpanSingleton R A 1) r • m ∈ N

Tactic:
rw [LinearMap.toSpanSingleton_apply, smul_one_smul]

Goal state after:
case refine_1
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
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ r • m ∈ N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
⊢ (M ^ n).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ n * M.toAddSubmonoid

Tactic:
cases n with
    | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
    | succ n => rw [ih n.succ_ne_zero]

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

Goal state before:
pp: case refine_2
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
r : S
x : M
r_in : r ∈ s
x_in : x ∈ restrictScalars S N
⊢ r • x ∈ restrictScalars S (⇑(algebraMap S R) '' s • N)

Tactic:
· rw [restrictScalars_mem, ← algebraMap_smul R r]
    exact mem_set_smul_of_mem_mem (Set.mem_image_of_mem _ r_in) x_in

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
hab : b ∣ a
⊢ b * (a / b) = a

Tactic:
by
  rw [← mul_div_assoc _ hab, mul_div_cancel_left₀ _ hb]

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

Goal state before:
pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
⊢ ∀ (a : R),
    ∀ x ∈ span R (↑I • Set.range f),
      (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) →
        ∃ a_2, ∃ (_ : ∀ (i : ι), a_2 i ∈ I), (a_2.sum fun i c ↦ c • f i) = a • x

Tactic:
rintro c x - ⟨a, ha, rfl⟩
    refine ⟨c • a, fun i => I.mul_mem_left c (ha i), ?_⟩
    rw [Finsupp.sum_smul_index, Finsupp.smul_sum] <;> intros <;> simp only [zero_smul, mul_smul]

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

Goal state before:
pp: case mpr.inl
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hx : x = 0
⊢ lcm 0 y = 0

Tactic:
lcm_zero_left

Goal state after:
case mpr.inl
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hx : x = 0
⊢ 0 = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y r s : R
hs : y = gcd x y * s
g : R
h : ¬g = 0
hr : x = g * r
⊢ g * (x * y / g) = x * y

Tactic:
subst hr

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
y r s g : R
h : ¬g = 0
hs : y = gcd (g * r) y * s
⊢ g * (g * r * y / g) = g * r * y
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inr.inr
R : Type u
inst✝ : EuclideanDomain R
b c d : R
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 : R
⊢ c * k1 * b / (c * d) = c * k1 / c * (b / d)

Tactic:
obtain ⟨k2, rfl⟩ := hbd

Goal state after:
case inr.inr
R : Type u
inst✝ : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_2
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ ∀ (a_1 : β) (s : Finset β),
    a_1 ∉ s →
      (s.gcd fun x ↦ a * f x) = normalize a * s.gcd f →
        ((insert a_1 s).gcd fun x ↦ a * f x) = normalize a * (insert a_1 s).gcd f

Tactic:
intro b t _ h
      rw [gcd_insert, gcd_insert, h, ← gcd_mul_left]
      apply ((normalize_associated a).mul_right _).gcd_eq_right

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
⊢ ∃ y ∈ J, f y = x

Tactic:
rcases surj x with ⟨x', hx'⟩

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
x' : A
hx' : f x' = x
⊢ ∃ y ∈ J, f y = x
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case right
A : Type u_1
B : Type u_2
inst✝¹ : Ring A
inst✝ : Ring B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : f x' = x
y : A
hy : y ∈ RingHom.ker f
z : A
hz : z ∈ J
hyz : y + z = x'
⊢ f z = x

Tactic:
simpa [← hx', ← hyz, ← RingHom.mem_ker] using hy

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ c ^ k = d₁ ^ k * d₂ ^ k

Tactic:
hc

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ (d₁ * d₂) ^ k = d₁ ^ k * d₂ ^ k
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf✝ : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
c : α
⊢ c ∉ f

Tactic:
hc

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf✝ : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
c : α
hc : c ∈ f
⊢ False
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a b c : α
⊢ lcm (b * a) (c * a) = lcm b c * normalize a

Tactic:
by simp only [mul_comm, lcm_mul_left]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
⊢ g₁ = g₂

Tactic:
have hgcd : g₁.gcd = g₂.gcd := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [dvd_gcd, gcd_dvd_left, gcd_dvd_right]
    have hlcm : g₁.lcm = g₂.lcm := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [lcm_dvd, dvd_lcm_left, dvd_lcm_right]
    cases g₁
    cases g₂
    dsimp only at hgcd hlcm
    simp only [hgcd, hlcm]

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ RightInverse (induced_map I ↑e.symm) (induced_map I ↑e)

Tactic:
by rintro ⟨a⟩; exact congr_arg _ (e.right_inv ..)

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Subsingleton

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
s : { s // LinearIndepOn R id s }
⊢ Cardinal.mk ↑↑s ≤ ⊥

Tactic:
by simp [(linearIndependent_subsingleton_iff _).mp s.2]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NormalizationMonoid R
I : Ideal R
inst✝ : IsPrincipal I
⊢ ∃ x, normalize x = x ∧ I = span {x}

Tactic:
by
  obtain ⟨x, rfl⟩ := ‹I.IsPrincipal›
  refine ⟨normalize x, normalize_idem x, le_antisymm ?_ ?_⟩ <;>
  simp [Ideal.mem_span_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
⊢ ∀ (a : Associates α), Quotient.map₂ lcm ⋯ 0 a = 0

Tactic:
rintro ⟨a⟩; exact congr_arg Associates.mk <| lcm_zero_left _

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
L L' : Submodule R M
inst✝ : Module.Finite R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ ↑(finrank R ↥L') < ℵ₀

Tactic:
exact natCast_lt_aleph0

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
⊢ L * (M + N) = L * M + L * N

Tactic:
ext
  apply dotProduct_add

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ i * (z * x + i ^ n) + y * x = 1

Tactic:
hz,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ i * 1 + y * x = 1
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
⊢ A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y

Tactic:
ext
  apply dotProduct_add

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
⊢ x ᵥ* (A + B) = x ᵥ* A + x ᵥ* B

Tactic:
ext
  apply dotProduct_add

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (toMultiset f) = f.sum fun x n ↦ Multiset.count a (n • {x})

Tactic:
rw [toMultiset_apply]; exact map_sum (Multiset.countAddMonoidHom a) _ f.support

Goal state after:
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α✝ : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : NonAssocSemiring α✝
inst✝³ : NonAssocSemiring β
inst✝² : NonAssocSemiring γ
α : Type ?u.30
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
x✝¹ x✝ : Matrix m m αᵐᵒᵖ
i✝ j✝ : m
⊢ unop (op ((x✝¹ * x✝)ᵀ.map unop)) i✝ j✝ = unop (op (x✝¹ᵀ.map unop) * op (x✝ᵀ.map unop)) i✝ j✝

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: α : Type u_14
inst✝¹ : MulOne α
inst✝ : AddCommMonoid α
x✝² : IsStablyFiniteRing αᵐᵒᵖ
n : ℕ
x✝¹ x✝ : Matrix (Fin n) (Fin n) α
i✝ j✝ : Fin n
⊢ { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun (x✝¹ * x✝) i✝ j✝ =
    ({ toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝¹ *
        { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝)
      i✝ j✝

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ ∀ {x : R}, x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} → -x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
rintro _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨-x, ⟨neg_mem _ hx, ⟨-y, ⟨neg_mem _ hy, by abel⟩⟩⟩⟩

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ (sSup S).toSubsemiring = sSup (toSubsemiring '' S)

Tactic:
rw [h, sSup_image, ← Subsemiring.closure_sUnion, sSup_def, adjoin_toSubsemiring]

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ ⋃₀ (SetLike.coe '' S)) =
    Subsemiring.closure (⋃₀ (SetLike.coe '' S))