mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : { f // IsIdempotentElem f ∧ range f = p }
x✝ : ↥p
x : E
hx : x ∈ p
⊢ ↑((codRestrict p ↑f ⋯) ↑⟨x, hx⟩) = ↑⟨x, hx⟩

Tactic:
by
      obtain ⟨x, rfl⟩ := f.2.2.symm ▸ hx
      exact DFunLike.congr_fun f.2.1 x

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
R : SetRel α α
inst✝ : R.IsRefl
⊢ SetRel.id ⊆ R

Tactic:
by rintro ⟨_, _⟩ rfl; exact R.rfl

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
⊢ (x, y) ∈ r

Tactic:
obtain hm | hm | hm := lt_trichotomy m.1 i.1

Goal state after:
case inl
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m < ↑i
⊢ (x, y) ∈ r

case inr.inl
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m = ↑i
⊢ (x, y) ∈ r

case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i < ↑m
⊢ (x, y) ∈ r
Module: Mathlib.Order.RelSeries

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

Tactic:
refine i.lastCases ?_ fun _ ↦ by dsimp only [smash]; apply Fin.addCases_left
  change p.smash q h (Fin.natAdd p.length (0 : Fin (q.length + 1))) = _
  simpa only [smash, Fin.addCases_right] using! h.symm

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P₂
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R₂ P₂
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
r : R
x p q : M ⊗[R] N
ih1 : (liftAux f') (r • p) = σ₁₂ r • (liftAux f') p
ih2 : (liftAux f') (r • q) = σ₁₂ r • (liftAux f') q
⊢ σ₁₂ r • (liftAux f') p + σ₁₂ r • (liftAux f') q = σ₁₂ r • ((liftAux f') p + (liftAux f') q)

Tactic:
smul_add

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

Goal state before:
pp: case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
hy✝ : y✝ ∈ closure (↑N ∪ ↑P)
h1 : m • x✝ ∈ M • N ⊔ M • P
h2 : m • y✝ ∈ M • N ⊔ M • P
⊢ m • (x✝ + y✝) ∈ M • N ⊔ M • P

Tactic:
smul_add

Goal state after:
case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
hy✝ : y✝ ∈ closure (↑N ∪ ↑P)
h1 : m • x✝ ∈ M • N ⊔ M • P
h2 : m • y✝ ∈ M • N ⊔ M • P
⊢ m • x✝ + m • y✝ ∈ M • N ⊔ M • P
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ ∀ (x y : A),
    x ∈ closure (↑N ∪ ↑P) →
      y ∈ closure (↑N ∪ ↑P) → m • x ∈ M • N ⊔ M • P → m • y ∈ M • N ⊔ M • P → m • (x + y) ∈ M • N ⊔ M • P

Tactic:
· intro _ _ _ _ h1 h2; rw [smul_add]; exact add_mem h1 h2

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
x y : A
⊢ t • x ∈ ⨆ i, T • S i → t • y ∈ ⨆ i, T • S i → t • (x + y) ∈ ⨆ i, T • S i

Tactic:
smul_add

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
x y : A
⊢ t • x ∈ ⨆ i, T • S i → t • y ∈ ⨆ i, T • S i → t • x + t • y ∈ ⨆ i, T • S i
Module: Mathlib.Data.Set.Semiring

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ up (⇑f '' down 1) = 1

Tactic:
by
    rw [down_one, image_one, map_one, singleton_one, up_one]

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
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • (m₁ + m₂) ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
smul_add

Goal state after:
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
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • m₁ + r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
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
r : R
h : IsUnit r
| 1

Tactic:
rw [one_eq_span, ← span_singleton_smul_eq h, ← algebraMap_eq_smul_one]

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
h : IsUnit r
| R ∙ (algebraMap R A) r
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
x : R
⊢ (∃ x_1 ∈ I.prod J, (RingHom.fst R S) x_1 = x) → x ∈ I

Tactic:
rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.1

Goal state after:
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.prod ⊤).IsPrime
x y : R
hxy : x * y ∈ I
⊢ (x * y, 1 * 1) ∈ I.prod ⊤

Tactic:
mul_one,

Goal state after:
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
⊢ (x * y, 1) ∈ I.prod ⊤
Module: Mathlib.Algebra.Algebra.Operations

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

Tactic:
algebraMap_smul

Goal state after:
case refine_1.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✝ ∈ ⇑(algebraMap S R) '' s • N
x : M
r : S
r_in : r ∈ s
x_in : x ∈ N
⊢ r • x ∈ s • restrictScalars S N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1.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
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
c : R →₀ ↥N
c_supp : ↑c.support ⊆ ⇑(algebraMap S R) '' s
hc : r • y = ↑(c.sum fun r m ↦ r • m)
u : S
u_in' : u ∈ s
u_in : (algebraMap S R) u ∈ c.support
⊢ (algebraMap S R) u • ↑(c ((algebraMap S R) u)) ∈ s • restrictScalars S N

Tactic:
algebraMap_smul

Goal state after:
case refine_1.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
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
c : R →₀ ↥N
c_supp : ↑c.support ⊆ ⇑(algebraMap S R) '' s
hc : r • y = ↑(c.sum fun r m ↦ r • m)
u : S
u_in' : u ∈ s
u_in : (algebraMap S R) u ∈ c.support
⊢ u • ↑(c ((algebraMap S R) u)) ∈ s • restrictScalars S N
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ ((∃ p, p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ p, p.IsPrime ∧ I = ⊤.prod p) → I.IsPrime

Tactic:
rintro (⟨p, ⟨h, rfl⟩⟩ | ⟨p, ⟨h, rfl⟩⟩)
    · exact isPrime_ideal_prod_top
    · exact isPrime_ideal_prod_top'

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Orzech

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ⇑f
x y : N
⊢ x = y

Tactic:
have h := IsNoetherian.injective_of_surjective_of_injective f _ i LinearMap.fst_surjective

Goal state after:
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ⇑f
x y : N
h : Injective ⇑(LinearMap.fst R M N)
⊢ x = y
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
⊢ (∃ x ∈ pi I, (Pi.evalRingHom R i) x = r) → r ∈ I i

Tactic:
rintro ⟨r, hr, rfl⟩

Goal state after:
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : (x : ι) → R x
hr : r ∈ pi I
⊢ (Pi.evalRingHom R i) r ∈ I i
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)

Tactic:
xgcd,

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ xgcdAux x 1 0 y 0 1 = (gcd x y, (xgcdAux x 1 0 y 0 1).2)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m : M
hm : m ∈ span R T
x✝³ x✝² : M
x✝¹ : x✝³ ∈ span R T
x✝ : x✝² ∈ span R T
h₁ : ∀ r ∈ Ideal.span S, r • x✝³ ∈ span R (S • T)
h₂ : ∀ r ∈ Ideal.span S, r • x✝² ∈ span R (S • T)
r : R
hr : r ∈ Ideal.span S
⊢ r • (x✝³ + x✝²) ∈ span R (S • T)

Tactic:
smul_add

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m : M
hm : m ∈ span R T
x✝³ x✝² : M
x✝¹ : x✝³ ∈ span R T
x✝ : x✝² ∈ span R T
h₁ : ∀ r ∈ Ideal.span S, r • x✝³ ∈ span R (S • T)
h₂ : ∀ r ∈ Ideal.span S, r • x✝² ∈ span R (S • T)
r : R
hr : r ∈ Ideal.span S
⊢ r • x✝³ + r • x✝² ∈ span R (S • T)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m : M
hm : m ∈ span R T
x✝³ x✝² : M
x✝¹ : x✝³ ∈ span R T
x✝ : x✝² ∈ span R T
h₁ : ∀ r ∈ Ideal.span S, r • x✝³ ∈ span R (S • T)
h₂ : ∀ r ∈ Ideal.span S, r • x✝² ∈ span R (S • T)
r : R
hr : r ∈ Ideal.span S
⊢ r • (x✝³ + x✝²) ∈ span R (S • T)

Tactic:
by rw [smul_add]; exact add_mem (h₁ r hr) (h₂ r hr)

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
r' : R
m : M
hm : m ∈ span R T
mem : ∀ r ∈ Ideal.span S, r • m ∈ span R (S • T)
r : R
hr : r ∈ Ideal.span S
⊢ r • r' • m ∈ span R (S • T)

Tactic:
rw [← mul_smul]; exact mem _ (Ideal.mul_mem_right _ _ hr)

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0

Tactic:
mul_one,

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a + b * 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1

Tactic:
mul_one,

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : x = 0 ∧ y = 0
⊢ y = 0

Tactic:
exact hgxy.2

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

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : c = 0
⊢ a * b / (a * c) = b / c

pp: case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c

Tactic:
· simp [hc]

Goal state after:
case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
I : Ideal S
N : Submodule R M
⊢ restrictScalars S (Ideal.map (algebraMap S R) I • N) = I • restrictScalars S N

Tactic:
have := N.restrictScalars_image_smul_eq (I : Set S)
  rw [coe_set_smul] at this
  rw [Ideal.map, span_smul_eq, ← this]

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ (s.card = s.card ∧ ∀ (b : α), b ∈ s → b = s.gcd * 1) ∧ (replicate s.card 1).gcd = 1

Tactic:
mul_one,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∀ (x : α), x ∈ s → x = 0
⊢ (s.card = s.card ∧ ∀ (b : α), b ∈ s → b = s.gcd) ∧ (replicate s.card 1).gcd = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ I ⊔ J = ⊤

Tactic:
rw [eq_top_iff_one]

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ I ⊔ J
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : ¬gcd x y = 0
x' : α
ex : x = gcd x y * x'
y' : α
ey : y = gcd x y * y'
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')

Tactic:
exact ⟨x', y', ex, ey, isUnit_gcd_of_eq_mul_gcd ex ey h⟩

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ g, s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : x * f a * ↑u + y * s.gcd f * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a

Tactic:
mul_comm x,

Goal state after:
case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ g, s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * ↑u + y * s.gcd f * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i j : ι
hfji : f j ≤ f i
u : Finset ι
ih : I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i u, I ≤ f i_1
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
h' : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ k ∈ ↑(insert i u), ↑(f k)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i (insert j u), I ≤ f i_1

Tactic:
refine ih.imp id (Or.imp id (Exists.imp fun k => ?_))

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i j : ι
hfji : f j ≤ f i
u : Finset ι
ih : I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i u, I ≤ f i_1
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
h' : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ k ∈ ↑(insert i u), ↑(f k)
k : ι
⊢ k ∈ insert i u ∧ I ≤ f k → k ∈ insert i (insert j u) ∧ I ≤ f k
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
S : Set α
⊢ S.matrix = ⇑of.symm ⁻¹' univ.pi fun x ↦ univ.pi fun x ↦ S

Tactic:
by
  ext
  simp [Set.mem_matrix]

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

Goal state before:
pp: case mpr
K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
x : M
inst✝ : Module.Finite K ↥(span K s)
c : M →₀ K
hcs : ↑c.support ⊆ s
hx : (c.sum fun mi r ↦ r • mi) = x
⊢ x ∈ span K s

Tactic:
exact mem_span_set.mpr ⟨c, hcs, hx⟩

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
⊢ ∃ b, b ≠ 0 ∧ b ⬝ᵥ a = 0

Tactic:
obtain ⟨i, j, hij⟩ : ∃ i j : m, i ≠ j := nontrivial_iff.mp ‹_›
  classical
  use if a i = 0 then Pi.single i 1 else if a j = 0 then Pi.single j 1 else
    fun k => if k = i then a j else if k = j then - a i else 0
  split_ifs with h h2
  · simp [h]
  · simp [h2]
  · refine ⟨Function.ne_iff.mpr ⟨i, by simp [h2]⟩, ?_⟩
    simp [dotProduct, Finset.sum_ite, Finset.sum_eq_ite i, hij.symm, mul_comm (a i)]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ Fintype (ChooseBasisIndex R M)

Tactic:
by
  refine @Fintype.ofFinite _ ?_
  cases subsingleton_or_nontrivial R
  · have := Module.subsingleton R M
    rw [ChooseBasisIndex]
    infer_instance
  · exact Module.Finite.finite_basis (chooseBasis _ _)

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ (b.smulTower' c) ij = b ij.2 • c ij.1

Tactic:
by
  rw [smulTower', reindex_apply, smulTower_apply]; rfl

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = s.card * count x {a}

Tactic:
count_singleton

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = s.card * if x = a then 1 else 0
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ count a s = s.card * 1

Tactic:
mul_one,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ count a s = s.card
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)

Tactic:
refine f.induction ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (toMultiset 0) = toMultiset (mapDomain g 0)

case refine_2
α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        Multiset.map g (toMultiset f) = toMultiset (mapDomain g f) →
          Multiset.map g (toMultiset (single a b + f)) = toMultiset (mapDomain g (single a b + f))
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ (toMultiset f).prod = f.prod fun a n ↦ a ^ n

Tactic:
refine f.induction ?_ ?_

Goal state after:
case refine_1
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ (toMultiset 0).prod = prod 0 fun a n ↦ a ^ n

case refine_2
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        ((toMultiset f).prod = f.prod fun a n ↦ a ^ n) →
          (toMultiset (single a b + f)).prod = (single a b + f).prod fun a n ↦ a ^ n
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ (toMultiset f).toFinset = f.support

Tactic:
refine f.induction ?_ ?_

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ (toMultiset 0).toFinset = support 0

case refine_2
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 → (toMultiset f).toFinset = f.support → (toMultiset (single a b + f)).toFinset = (single a b + f).support
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: n : Type u_3
R : Type u_7
α : Type u_11
β : Type u_12
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ ((algebraMap R (Matrix n n α)) r).map f = (algebraMap R (Matrix n n β)) r

Tactic:
rw [algebraMap_eq_diagonal, algebraMap_eq_diagonal, diagonal_map hf]

Goal state after:
n : Type u_3
R : Type u_7
α : Type u_11
β : Type u_12
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ (diagonal fun m ↦ f ((algebraMap R (n → α)) r m)) = diagonal ((algebraMap R (n → β)) r)