mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
suffices ¬ LinearIndependent R ![a • x + b • y, c • x + d • y] by simpa [h]
    rw [pair_iff]
    push Not
    by_cases hbd : b = 0 ∧ d = 0
    · simp only [hbd.1, hbd.2, zero_smul, add_zero]
      by_cases hac : a = 0 ∧ c = 0; · exact ⟨1, 0, by simp [hac.1, hac.2], by simp⟩
      refine ⟨c • 1, -a • 1, ?_, by aesop⟩
      simp only [smul_assoc, one_smul, neg_smul]
      module
    refine ⟨d • 1, -b • 1, ?_, by contrapose! hbd; simp_all⟩
    simp only [smul_add, smul_assoc, one_smul, smul_smul, mul_comm d, h]
    module

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
c : γ
⊢ c ∈ image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c

Tactic:
simp [image₂, and_assoc]

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : γ → β → γ
b : β
h : ∀ (a : γ), f a b = a
s : Finset γ
⊢ image (fun x ↦ x) s = s

Tactic:
image_id'

Goal state after:
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : γ → β → γ
b : β
h : ∀ (a : γ), f a b = a
s : Finset γ
⊢ s = s
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor
  · contrapose! +distrib
    rintro (hs | rfl)
    · exact hs.pow
    · simp
  · rintro ⟨rfl, hn⟩
    exact empty_pow hn

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
b : M
a✝ : b ∈ ⊤
a₂ : α
⊢ a₂ ∈ t → (lapply a₂ ∘ₗ lsingle a₁) b = 0

Tactic:
h₂

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
b : M
a✝ : b ∈ ⊤
a₂ : α
h₂ : a₂ ∈ t
⊢ (lapply a₂ ∘ₗ lsingle a₁) b = 0
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ (monomial m) a = (monomial n) b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

Tactic:
by
  rw [← toFinsupp_inj, toFinsupp_monomial, toFinsupp_monomial, single_inj]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a} = ⊤

Tactic:
apply top_unique

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ ⊤ ≤ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
⊢ ∀ (s : Finset ℕ), motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n)

Tactic:
apply Finset.induction

Goal state after:
case empty
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
⊢ motive (∑ n ∈ ∅, Polynomial.C (p.coeff n) * X ^ n)

case insert
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
⊢ ∀ (a : ℕ) (s : Finset ℕ),
    a ∉ s →
      motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n) → motive (∑ n ∈ insert a s, Polynomial.C (p.coeff n) * X ^ n)
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
h : s.Infinite
⊢ sSup s = ⊤

Tactic:
exact sSup_eq_top_of_infinite h

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

Goal state before:
pp: case inr.inr
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
hne : a ≠ 0
hι : Nonempty ι
⊢ a * ⨆ i, f i ≤ d

Tactic:
cases d with
  | top => simp
  | coe d =>
  have hlt : ⨆ i, f i < ⊤ := by
    rw [lt_top_iff_ne_top]
    intro htop
    obtain ⟨i, hi : d < f i⟩ := (iSup_eq_top ..).1 htop d (by simp)
    exact (((h i).trans_lt hi).trans_le (ENat.self_le_mul_left _ hne)).false
  obtain ⟨j, hj⟩ := exists_eq_iSup_of_lt_top hlt
  rw [← hj]
  apply h

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
b : ι
hb : f b = ⨅ x, f x
⊢ ∀ (b_1 : ℕ∞), (∀ (i : ι), b_1 ≤ a * f i) → b_1 ≤ a * f b

Tactic:
exact fun x h ↦ h _

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
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 : E
⊢ ↑f x ∈ p

Tactic:
simp_rw [← f.2.2]

Goal state after:
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 : E
⊢ ↑f x ∈ range ↑f
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : RelSeries r
⊢ ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) ((fun x ↦ ⟨x.toList, ⋯⟩) x)).toFun = x.toFun ∘ Fin.cast ⋯

Tactic:
by ext; dsimp; apply List.get_ofFn

Goal state after:
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
x y : B
⊢ g x + g y = g x + g (f (g y))

Tactic:
h₂

Goal state after:
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
x y : B
⊢ g x + g y = g x + g y
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
⊢ RelSeries.last p ≤ a → ↑p.length ≤ n

Tactic:
hlast

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
⊢ ↑p.length ≤ n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
⊢ RelSeries.last p = x → ↑p.length + 1 ≤ height y

Tactic:
hlast

Goal state after:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length + 1 ≤ height y
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
⊢ Function.Surjective ⇑f ↔ g = 0

Tactic:
by
  rw [← LinearMap.ker_eq_top, h.linearMap_ker_eq, LinearMap.range_eq_top]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
⊢ RelSeries.last p = x → ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length

Tactic:
hlast

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x : α), IsMax x

Tactic:
← krullDim_nonpos_iff_forall_isMax

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : ⟨i, hi⟩ ≤ ⟨j, hj⟩
⊢ p.toFun ⟨i, hi⟩ + ↑⟨j, hj⟩ ≤ p.toFun ⟨j, hj⟩ + ↑⟨i, hi⟩

Tactic:
simp only [Fin.mk_le_mk] at hij

Goal state after:
p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑⟨j, hj⟩ ≤ p.toFun ⟨j, hj⟩ + ↑⟨i, hi⟩
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a + coheight a)

Tactic:
krullDim_eq_iSup_height_of_nonempty,

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a) ≤ ↑(⨆ a, height a + coheight a)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℤ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : ⟨i, hi⟩ ≤ ⟨j, hj⟩
⊢ p.toFun ⟨i, hi⟩ + ↑↑⟨j, hj⟩ ≤ p.toFun ⟨j, hj⟩ + ↑↑⟨i, hi⟩

Tactic:
simp only [Fin.mk_le_mk] at hij

Goal state after:
p : LTSeries ℤ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑↑⟨j, hj⟩ ≤ p.toFun ⟨j, hj⟩ + ↑↑⟨i, hi⟩
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ krullDim α = ⨆ a, ↑(height a)

Tactic:
krullDim_eq_iSup_height_of_nonempty,

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ ↑(⨆ a, height a) = ⨆ a, ↑(height a)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
⊢ RelSeries.last p = ↑x → ↑p.length ≤ height x + 1

Tactic:
hlast

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
⊢ RelSeries.last p = x → ↑p.length + 1 ≤ height ↑x

Tactic:
hlast

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
⊢ RelSeries.last p = ↑x → ↑p.length ≤ height x

Tactic:
hlast

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
⊢ ↑p.length ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
⊢ RelSeries.last p = x → ↑p.length ≤ height ↑x

Tactic:
hlast

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length ≤ height ↑x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(height ⊤) = krullDim α + 1

Tactic:
krullDim_eq_iSup_height_of_nonempty,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(height ⊤) = ↑(⨆ a, height a) + 1
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✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ⇑f '' a * ⇑f '' as.prod = ⇑f '' a * (List.map (fun s ↦ ⇑f '' s) as).prod

Tactic:
image_list_prod _ _

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

Goal state before:
pp: case insert.mp
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a) →
    ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a

Tactic:
rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩
      refine ⟨Function.update g i x, ?_, ?_⟩
      · intro j hj
        obtain rfl | hj := Finset.mem_insert.mp hj
        · rwa [Function.update_self]
        · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
          exact hg hj
      · rw [Finset.prod_update_of_notMem hi, Function.update_self]

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

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = closure (↑M * ↑N)

Tactic:
by
  rw [← closure_mul_closure, closure_eq, closure_eq]

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

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

Tactic:
exact H.of_mul_left_left

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

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

Tactic:
exact H.of_mul_left_left

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

Goal state before:
pp: case h
x y : ℤ
h : IsCoprime x y
⊢ x * x.gcdA y + y * x.gcdB y = 1

Tactic:
← Int.gcd_eq_gcd_ab,

Goal state after:
case h
x y : ℤ
h : IsCoprime x y
⊢ ↑(x.gcd y) = 1
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
⊢ 1 ≤ toAddSubmonoid 1

Tactic:
rintro x ⟨n, rfl⟩

Goal state after:
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
n : ℕ
⊢ (Nat.castAddMonoidHom A) n ∈ toAddSubmonoid 1
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
⊢ (∃ r, x = (algebraMap R A) ↑r) → R ∙ x = 1

Tactic:
rintro ⟨r, rfl⟩; exact span_singleton_algebraMap_of_isUnit r.isUnit

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

Goal state before:
pp: case mp.inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
hI : ((map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)).IsPrime
h : map (RingHom.fst R S) I = ⊤
⊢ (∃ p, p.IsPrime ∧ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) = p.prod ⊤) ∨
    ∃ p, p.IsPrime ∧ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) = ⊤.prod p

Tactic:
right
      rw [h] at hI ⊢
      exact ⟨_, ⟨isPrime_of_isPrime_prod_top' hI, rfl⟩⟩

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (x * z - y) / z = x - y / z

Tactic:
rw [mul_comm x z]
  exact mul_sub_div_left _ _ _ h1 h2

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

Goal state before:
pp: case inr
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hy : y ≠ 0
⊢ x / y / z = x / (y * z)

Tactic:
exact (div_mul h1 h2).symm

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ K = ⊤
i : R
hi : i ∈ I ⊔ J
⊢ i ∈ I ⊔ J * K

Tactic:
rw [eq_top_iff_one] at h; rw [Submodule.mem_sup] at h hi ⊢
    obtain ⟨i1, hi1, k, hk, h⟩ := h; obtain ⟨i', hi', j, hj, rfl⟩ := hi
    refine ⟨_, add_mem hi' (mul_mem_left _ j hi1), _, mul_mem_mul hj hk, ?_⟩
    rw [add_assoc, ← mul_add, h, mul_one]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
⊢ I ⊔ J ^ n = ⊤

Tactic:
induction n with
  | zero => simp [J.pow_zero]
  | succ n ih => rwa [J.pow_succ, sup_mul_eq_of_coprime_left ih]

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

Goal state before:
pp: case succ.zero
R : Type u
inst✝ : Semiring R
ih : 0 ≠ 0 → ↑0 = ⊤
hn : 0 + 1 ≠ 0
⊢ ↑(0 + 1) = ⊤

Tactic:
rw [Nat.cast_one, one_eq_top]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
⊢ ∀ (x y : B), g (f_inv (x * y)) = g (f_inv x) * g (f_inv y)

Tactic:
intro x y
      rw [← map_mul g, ← sub_eq_zero, ← map_sub g, ← mem_ker]
      apply hg
      rw [mem_ker, map_sub f, sub_eq_zero, map_mul f]
      simp only [hf _]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ gcd 0 0

Tactic:
apply dvd_gcd

Goal state after:
case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ 0

case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ Associated (1 ^ k) a

Tactic:
rw [one_pow]

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ Associated 1 a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
this : a * b * ↑(Classical.choose ⋯) = a * ↑(Classical.choose ⋯) * (b * ↑(Classical.choose ⋯))
⊢ ↑(Classical.choose ⋯) = ↑(Classical.choose ⋯) * ↑(Classical.choose ⋯)

Tactic:
apply mul_left_cancel₀ (mul_ne_zero ha hb) _

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
this : a * b * ↑(Classical.choose ⋯) = a * ↑(Classical.choose ⋯) * (b * ↑(Classical.choose ⋯))
⊢ a * b * ↑(Classical.choose ⋯) = a * b * (↑(Classical.choose ⋯) * ↑(Classical.choose ⋯))
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f

Tactic:
refine ⟨fun h n => fun f hf => ?_, fun h => ⟨@fun n m f hf => ?_⟩⟩

Goal state after:
case refine_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ⇑f
⊢ False

case refine_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ⇑f
⊢ n ≤ m
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
⊢ Module.rank R M = 0

Tactic:
rw [Module.rank, ← bot_eq_zero, eq_bot_iff]
  exact ciSup_le fun s ↦ by simp [(linearIndependent_subsingleton_iff _).mp s.2]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
S : Submodule R N
hI : (comap f S).IsPrincipal
⊢ S.IsPrincipal

Tactic:
← Submodule.map_comap_eq_of_surjective hf S

Goal state after:
R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
S : Submodule R N
hI : (comap f S).IsPrincipal
⊢ (Submodule.map f (comap f S)).IsPrincipal
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
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
have := nontrivial_of_invariantBasisNumber R
  cases fintypeOrInfinite J
  · rw [← Cardinal.lift_le, Cardinal.mk_range_eq_of_injective v.injective, Cardinal.mk_fintype J]
    convert! Cardinal.lift_le.{v}.2 (basis_le_span' v hJ)
    simp
  · let S : J → Set ι := fun j => ↑(v.repr j).support
    let S' : J → Set M := fun j => v '' S j
    have hs : range v ⊆ ⋃ j, S' j := by
      intro b hb
      rcases mem_range.1 hb with ⟨i, hi⟩
      have : span R J ≤ comap v.repr.toLinearMap (Finsupp.supported R R (⋃ j, S j)) :=
        span_le.2 fun j hj x hx => ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩
      rw [hJ] at this
      replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial
      rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single _ one_ne_zero] at this
      · subst b
        rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩
        exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩
    refine le_of_not_gt fun IJ => ?_
    suffices #(⋃ j, S' j) < #(range v) by exact not_le_of_gt this ⟨Set.embeddingOfSubset _ _ hs⟩
    refine lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk
      (Cardinal.sum_le_sum _ (fun _ => ℵ₀) ?_)) ?_
    · exact fun j => (Cardinal.lt_aleph0_of_finite _).le
    · simpa

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

Goal state before:
pp: case pos
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ diagonal d (e j) (e j) = diagonal (d ∘ e) j j

Tactic:
diagonal_apply_eq,

Goal state after:
case pos
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ d (e j) = diagonal (d ∘ e) j j