mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ g '' image2 f ↑s ↑t = image2 f' (g₁ '' ↑s) (g₂ '' ↑t)

Tactic:
exact image_image2_distrib h_distrib

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
N : Type u_7
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Monoid M
inst✝ : Monoid N
f : R →+* S
g : M →* N
⊢ (mapRingHom N f).comp (mapDomainRingHom R g) = (mapDomainRingHom S g).comp (mapRingHom M f)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Monoid N
m : M
n : N
r : R
⊢ curryRingEquiv.symm (single m (single n r)) = single (m, n) r

Tactic:
by
  simp [curryRingEquiv]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), f (x * y) = f x * f y
⊢ UniqueMul (map f A) (map f B) (f a0) (f b0) ↔ UniqueMul A B a0 b0

Tactic:
classical simp_rw [← mulHom_image_iff ⟨f, mul⟩ f.2, Finset.map_eq_image]; rfl

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
L✝ M✝ : Sublattice α
f : LatticeHom α β
s t : Set α
a b : α
L M : Sublattice α
h : (fun L ↦ L.carrier) L = (fun L ↦ L.carrier) M
⊢ L = M

Tactic:
cases L

Goal state after:
case mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
L M✝ : Sublattice α
f : LatticeHom α β
s t : Set α
a b : α
M : Sublattice α
carrier✝ : Set α
supClosed'✝ : SupClosed carrier✝
infClosed'✝ : InfClosed carrier✝
h :
  (fun L ↦ L.carrier) { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ } =
    (fun L ↦ L.carrier) M
⊢ { carrier := carrier✝, supClosed' := supClosed'✝, infClosed' := infClosed'✝ } = M
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Semiring R
inst✝ : DecidableEq ι
⊢ LinearIndependent R fun i ↦ single i 1

Tactic:
rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
  exact Pi.linearIndependent_single (fun (_ : ι) (_ : Unit) ↦ (1 : R))
    <| by simp +contextual [Fintype.linearIndependent_iffₛ]

Goal state after:
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
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl i.range q
x : F
⊢ (linearProjOfIsCompl q i hi h) (i x) = x

Tactic:
obtain ⟨ix, rfl⟩ := (LinearEquiv.ofInjective i hi).symm.surjective x
  simp [linearProjOfIsCompl]

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
n : ℕ
⊢ (↑↑n).succ = ↑n + 1

Tactic:
succ_coe,

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
n : ℕ
⊢ Order.succ ↑n = ↑n + 1
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ∅.dom = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ∅.cod = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
⊢ dom Set.univ = Set.univ

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
⊢ cod Set.univ = Set.univ

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
⊢ SetRel.id.inv = SetRel.id

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : SetRel α β
S : SetRel β γ
t : SetRel γ δ
⊢ R ○ S ○ t = R ○ (S ○ t)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R ○ SetRel.id = R

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ SetRel.id ○ R = R

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
⊢ (R ○ S).inv = S.inv ○ R.inv

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
⊢ R ○ ∅ = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
S : SetRel β γ
⊢ ∅ ○ S = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
R : SetRel α β
S : ι → SetRel β γ
⊢ R ○ ⋃ i, S i = ⋃ i, R ○ S i

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
R : ι → SetRel α β
S : SetRel β γ
⊢ (⋃ i, R i) ○ S = ⋃ i, R i ○ S

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
𝒮 : Set (SetRel β γ)
⊢ R ○ ⋃₀ 𝒮 = ⋃ S ∈ 𝒮, R ○ S

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ℛ : Set (SetRel α β)
S : SetRel β γ
⊢ ⋃₀ ℛ ○ S = ⋃ R ∈ ℛ, R ○ S

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t₁ t₂ : Set β
ht : (t₁ ∩ t₂).Nonempty
s : Set α
u : Set γ
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.image ∅ = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.preimage ∅ = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.image Set.univ = R.cod

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.preimage Set.univ = R.dom

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s₁ s₂ : Set α
⊢ R.image (s₁ ∪ s₂) = R.image s₁ ∪ R.image s₂

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
R : SetRel α β
s : ι → Set α
⊢ R.image (⋃ i, s i) = ⋃ i, R.image (s i)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
S : Set (Set α)
⊢ R.image (⋃₀ S) = ⋃ s ∈ S, R.image s

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
⊢ R.preimage (t₁ ∪ t₂) = R.preimage t₁ ∪ R.preimage t₂

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
R : SetRel α β
t : ι → Set β
⊢ R.preimage (⋃ i, t i) = ⋃ i, R.preimage (t i)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
T : Set (Set β)
⊢ R.preimage (⋃₀ T) = ⋃ t ∈ T, R.preimage t

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s : Set α
⊢ SetRel.id.image s = s

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s : Set α
⊢ SetRel.id.preimage s = s

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
s : Set α
⊢ (R ○ S).image s = S.image (R.image s)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
u : Set γ
⊢ (R ○ S).preimage u = R.preimage (S.preimage u)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ ∅.image s = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
⊢ ∅.preimage t = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
⊢ image Set.univ s = Set.univ

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
h : R.dom ⊆ s
⊢ R.image s = R.cod

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
h : R.cod ⊆ t
⊢ R.preimage t = R.dom

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ R.image (s ∩ R.dom) = R.image s

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ R.preimage (t ∩ R.cod) = R.preimage t

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ R.image s = ⋃ x ∈ s, {y | (x, y) ∈ R}

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ R.preimage t = ⋃ y ∈ t, {x | (x, y) ∈ R}

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
⊢ R.core (t₁ ∩ t₂) = R.core t₁ ∩ R.core t₂

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.core Set.univ = Set.univ

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: β : Type u_2
t : Set β
⊢ SetRel.id.core t = t

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
u : Set γ
⊢ (R ○ S).core u = R.core (S.core u)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
x : α × α
x✝² x✝¹ x✝ : α
⊢ (x✝², x✝¹) ∈ {x} → (x✝¹, x✝) ∈ {x} → (x✝², x✝) ∈ {x}

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
⊢ graph id = SetRel.id

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
⊢ graph (f ∘ g) = graph g ○ graph f

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b, (a, b) ∈ R
f : α → β
hf : ∀ (x : α), (x, f x) ∈ R
⊢ ∀ (y : α → β), (fun f ↦ Function.graph f = R) y → y = f

Tactic:
by aesop

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

Goal state before:
pp: case refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
⊢ TwoUniqueProds (G × H)

Tactic:
refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he ↦ Prod.ext ?_ ?_)
      (TwoUniqueProds.instForall <| I G H)

Goal state after:
case refine_1.refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ x.1 = y.1

case refine_1.refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ x.2 = y.2
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ height x = ↑n + 1 ↔ height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n

Tactic:
by
  wlog hfin : height x < ⊤
  · simp_all [← Nat.cast_add_one, -Nat.cast_add]
  simp only [hfin, true_and]
  trans n < height x ∧ height x ≤ n + 1
  · rw [le_antisymm_iff, and_comm]
    simp [ENat.add_one_le_iff]
  · congr! 1
    · exact coe_lt_height_iff hfin
    · simpa [hfin, ENat.lt_add_one_iff] using height_le_coe_iff (x := x) (n := n + 1)

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
cases isEmpty_or_nonempty α
  · simp [krullDim_eq_bot]
  cases finiteDimensionalOrder_or_infiniteDimensionalOrder α
  · rw [krullDim_eq_length_of_finiteDimensionalOrder, Nat.cast_le]
    constructor
    · exact fun H ↦ ⟨(LTSeries.longestOf α).take ⟨_, Nat.lt_succ_of_le H⟩, rfl⟩
    · exact fun ⟨l, hl⟩ ↦ hl ▸ l.longestOf_is_longest
  · simpa [krullDim_eq_top] using SetRel.InfiniteDimensional.exists_relSeries_with_length n

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case hab
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun i ≤ ?b

Tactic:
exact p.monotone (Fin.le_last _)

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
x : Submodule R M
m : M
⊢ (∃ m_1 ∈ x, m = 1 • m_1) → m ∈ x

Tactic:
by rintro ⟨_, h, rfl⟩; rwa [one_smul]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s : Set R
x y : Submodule R M
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ s → n ∈ x + y → r • n ∈ s • x + s • y

Tactic:
rintro r m hr hm

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
m : M
hr : r ∈ s
hm : m ∈ x + y
⊢ r • m ∈ s • x + s • y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime (x • y) z
a b : R
h : a * x • y + b * z = 1
⊢ x • a * y + b * z = 1

Tactic:
rwa [smul_mul_assoc, ← mul_smul_comm]

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

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

Tactic:
mul_add_right_right_iff,

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

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

Tactic:
mul_add_right_right_iff,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime x (-y) ↔ IsRelPrime x y
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
r : A
hr : r ∈ 1
m : M
hm : m ∈ N
⊢ r • m ∈ N

Tactic:
obtain ⟨r, rfl⟩ := hr
    rw [LinearMap.toSpanSingleton_apply, smul_one_smul]; exact N.smul_mem r hm

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
inst✝ : IsScalarTower R A A
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊥ ^ (n + 2) = ⊥

Tactic:
by rw [Submodule.pow_succ, bot_pow n.succ_ne_zero, bot_mul]

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
inst✝¹ : IsScalarTower R A A
inst✝ : IsReduced A
M : Submodule R A
n : ℕ
hn : n ≠ 0
⊢ M = ⊥ → M ^ n = ⊥

Tactic:
by aesop

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

Goal state before:
pp: case refine_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ ↑t
j : I
hj : j ∈ ↑t
h : i ≠ j
⊢ j ∈ t \ {i}

Tactic:
exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h (Finset.mem_singleton.mp f).symm⟩

Goal state after:
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
b : I
t : Finset I
hbt : b ∉ t
ih : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x

Tactic:
rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]

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

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
a✝ b✝ : A
ha : a✝ ∈ {x | ∀ y ∈ J, x * y ∈ I}
hb : b✝ ∈ {x | ∀ y ∈ J, x * y ∈ I}
y : A
hy : y ∈ J
⊢ (a✝ + b✝) * y ∈ I

Tactic:
rw [add_mul]
        exact Submodule.add_mem _ (ha _ hy) (hb _ hy)

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 S
h : I.IsPrime
⊢ (⊤.prod I).IsPrime

Tactic:
let : IsPrime (prod I (⊤ : Ideal R)) := isPrime_ideal_prod_top
  rw [← map_prodComm_prod]
  -- Note: couldn't synthesize the right instances without the `R` and `S` hints
  exact map_isPrime_of_equiv (RingEquiv.prodComm (R := S) (S := R))

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
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
x✝ : ∃ f, ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x) (f x) = r x
r' : ι → (x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x) (r' x) = r x
this : Fintype ι
i : ι
⊢ (Pi.evalRingHom R i) (r' i) = ∑ c, (Pi.single c 1 * r' c) i

Tactic:
Fintype.sum_eq_single i fun j ne ↦ by simp [ne]

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
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
x✝ : ∃ f, ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x) (f x) = r x
r' : ι → (x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x) (r' x) = r x
this : Fintype ι
i : ι
⊢ (Pi.evalRingHom R i) (r' i) = (Pi.single i 1 * r' i) i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_1.refine_1
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)
y : R
hy : y ∈ ↑I
i j : ι
this : DecidableEq ι := Classical.decEq ι
⊢ (Finsupp.single i y) j ∈ I

Tactic:
rw [Finsupp.single_apply]

Goal state after:
case mp.refine_1.refine_1
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)
y : R
hy : y ∈ ↑I
i j : ι
this : DecidableEq ι := Classical.decEq ι
⊢ (if i = j then y else 0) ∈ I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
I : Ideal R
inst✝ : Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal (Ideal.map f I)

Tactic:
obtain ⟨x, rfl⟩ := Submodule.IsPrincipal.principal I

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ Submodule.IsPrincipal (Ideal.map f (R ∙ x))
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a✝ : Nontrivial α
⊢ normUnit (0 * ↑(normUnit 0)) = 1

pp: case inr
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
h : a ≠ 0
⊢ normUnit (a * ↑(normUnit a)) = 1

Tactic:
· rw [normUnit_zero, zero_mul, normUnit_zero]

Goal state after:
case inr
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
h : a ≠ 0
⊢ normUnit (a * ↑(normUnit a)) = 1
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' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')

Tactic:
obtain ⟨x', ex⟩ := gcd_dvd_left x y

Goal state after:
case neg
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
h : ¬gcd x y = 0
x' : α
ex : x = gcd x y * x'
⊢ ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
f : α
hf : a = gcd a c * f
⊢ b = gcd a c * (e + f * d)

Tactic:
rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (ℕ →₀ R) →ₗ[R] Fin n → R
inj : Injective ⇑f
⊢ Injective ⇑(Finsupp.lmapDomain R R Fin.val ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R R (Fin (n + 1))).symm)

Tactic:
by simpa using! Finsupp.mapDomain_injective Fin.val_injective

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ Classical.choose ⋯ ∣ b

Tactic:
rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b),
        mul_dvd_mul_iff_right h_1]

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ a ∣ lcm a b