mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : f x' ∈ sInf (map f '' A)
hx : f x = f x'
this : ∀ I ∈ A, f x' ∈ map f I
⊢ x - x' ∈ RingHom.ker f

Tactic:
rw [RingHom.mem_ker, map_sub, hx, sub_self]

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

Goal state before:
pp: a b : ℕ
⊢ Associated (a * b) (a * b)

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
⊢ ↑n = ⊤

Tactic:
by
  induction n with
  | zero => exact (hn rfl).elim
  | succ n ih =>
    obtain rfl | n := n; · rw [Nat.cast_one, one_eq_top]
    rw [Nat.cast_succ, ih n.succ_ne_zero, add_eq_sup, top_sup_eq]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
⊢ ker (Pi.evalRingHom R i) = Ideal.span {1 - Pi.single i 1}

Tactic:
by
  refine le_antisymm (fun x hx ↦ ?_) (by simp [Ideal.span_le])
  simp only [RingHom.mem_ker, Pi.evalRingHom_apply] at hx
  rw [Ideal.mem_span_singleton]
  use x + Pi.single i 1
  simp [mul_add, sub_mul, one_mul, ← Pi.single_mul_left, hx]

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

Goal state before:
pp: case cons
ι : Type u_1
s✝ : Finset ι
f : ι → ℤ
a : ι
s : Finset ι
has : a ∉ s
ih : 0 ≤ s.gcd f
⊢ 0 ≤ ↑((f a).gcd (s.gcd f))

Tactic:
grind

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

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

Tactic:
rfl

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

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : ∏ i ∈ s, J i = ⨅ i ∈ s, J i
hp1 : (↑s).Pairwise (IsCoprime on J)
hp2 : ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ ∀ j ∈ s, IsCoprime (J a) (J j)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
k m n : α
⊢ gcd k (m * n) ∣ gcd k m * gcd k n

Tactic:
obtain ⟨m', n', hm', hn', h⟩ := exists_dvd_and_dvd_of_dvd_mul (gcd_dvd_right k (m * n))
  replace h : gcd k (m * n) = m' * n' := h
  rw [h]
  have hm'n' : m' * n' ∣ k := h ▸ gcd_dvd_left _ _
  apply mul_dvd_mul
  · have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n'
    exact dvd_gcd hm'k hm'
  · have hn'k : n' ∣ k := (dvd_mul_left n' m').trans hm'n'
    exact dvd_gcd hn'k hn'

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

Goal state before:
pp: case neg.succ
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b ^ (k + 1)) ∣ gcd a b ^ (k + 1)

Tactic:
rw [pow_succ', pow_succ']

Goal state after:
case neg.succ
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b * b ^ k) ∣ gcd a b * gcd a b ^ k
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : 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
⊢ ∃ d, Associated (d ^ k) a

Tactic:
obtain rfl | hk := k.eq_zero_or_pos

Goal state after:
case neg.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = c ^ 0
⊢ ∃ d, Associated (d ^ 0) a

case neg.inr
α : 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
hk : k > 0
⊢ ∃ d, Associated (d ^ k) a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case refl.refl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd✝¹ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝¹ : ∀ (a b : α), normalize (lcm a b) = lcm a b
normalize_gcd✝ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝ : ∀ (a b : α), normalize (lcm a b) = lcm a b
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝¹,
      normalize_lcm := normalize_lcm✝¹ } =
    { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝,
      normalize_lcm := normalize_lcm✝ }

Tactic:
rfl

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

Goal state before:
pp: case refl.refl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
a_norm : StrongNormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd✝¹ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝¹ : ∀ (a b : α), normalize (lcm a b) = lcm a b
normalize_gcd✝ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝ : ∀ (a b : α), normalize (lcm a b) = lcm a b
⊢ { toStrongNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝¹,
      normalize_lcm := normalize_lcm✝¹ } =
    { toStrongNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝,
      normalize_lcm := normalize_lcm✝ }

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a : α
a0 : a = 0
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a : α
a0 : a = 0
⊢ 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
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 + s.gcd f * y * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
b : α
hb : b ∈ s
⊢ b ≠ a

Tactic:
grind

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
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a

Tactic:
obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)
    obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)
    rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu
    obtain ⟨g, hg⟩ := ih
    refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
    rw [gcd_insert, sum_insert ha, ← hu, hg]
    simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]
    exact sum_congr rfl fun b hb ↦ congrArg (f b * ·) <|
      (Function.update_of_ne (show b ≠ a by grind) (x * u) (g · * (y * u))).symm

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
h : z ∈ S
y : R
hz : 1 = generator T * y
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T

Tactic:
exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)

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
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
have := nontrivial_of_invariantBasisNumber R

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
exact Or.inr (Or.inr ⟨i, Finset.mem_insert_self i t, ih⟩)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i✝ : m
j✝ : n
⊢ M.map id i✝ j✝ = M i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (g ∘ f) i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, (∀ (i : m) (j : n), A i j + b i j = 0) ∧ ∀ (i : m) (j : n), b i j + A i j = 0) ↔
    ∃ f, (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0

Tactic:
rfl

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✝¹ : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
have := nontrivial_of_invariantBasisNumber R

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this : Nontrivial R
⊢ #ι ≤ ↑(Fintype.card ↑w)
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i✝ : m
j✝ : n
⊢ Mᵀᵀ i✝ j✝ = M i✝ j✝

Tactic:
rfl

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
ι : 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

Goal state after:
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 = ⊤
this : Nontrivial R
⊢ #↑(range ⇑v) ≤ #↑J
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 = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
i : ι
this : ↑{i} ⊆ ⋃ j, S j
hb : v i ∈ range ⇑v
⊢ v i ∈ ⋃ j, S' j

Tactic:
rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩

Goal state after:
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 = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
i : ι
this : ↑{i} ⊆ ⋃ j, S j
hb : v i ∈ range ⇑v
j : ↑J
hj : i ∈ S j
⊢ v i ∈ ⋃ j, S' j
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case a
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
this : Nontrivial R
⊢ #ι ≤ #κ

Tactic:
exact infinite_basis_le_maximal_linearIndependent b v i m

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
ι : Type v
v : Basis ι R M
⊢ #ι = Module.rank R M

Tactic:
have := nontrivial_of_invariantBasisNumber R

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι = Module.rank R M
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
ι : Type w
inst✝ : Fintype ι
h : Basis ι R M
⊢ Module.rank R M = ↑(Fintype.card ι)

Tactic:
have := nontrivial_of_invariantBasisNumber R

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Fintype ι
h : Basis ι R M
this : Nontrivial R
⊢ Module.rank R M = ↑(Fintype.card ι)
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✝ : StrongRankCondition R
v : Basis ι R M
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)

Tactic:
have := nontrivial_of_invariantBasisNumber R

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)
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✝ : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
⊢ Module.rank R ↥(span R (range v)) = #↑(range v)

Tactic:
have := nontrivial_of_invariantBasisNumber R

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
⊢ Module.rank R ↥(span R (range v)) = #↑(range v)
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✝ : StrongRankCondition R
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
⊢ toENat (Module.rank R ↥(span R (v '' s))) = s.encard

Tactic:
rw [image_eq_range, ← hs.injOn.encard_image, ← toENat_cardinalMk, image_eq_range,
    ← rank_span hs.linearIndependent]

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

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝¹ : DecidableEq m
inst✝ : Zero α
i : m
r : α
j k : m
⊢ (if j = k then Pi.single i r j else 0) = if i = j ∧ i = k then r else 0

Tactic:
grind

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
⊢ (single i i c).diag j = Pi.single i c j

Tactic:
by_cases hij : i = j <;> (try rw [hij]) <;> simp [hij]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ⟨0, ⋯⟩ = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
A : Type u_3
ι : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
b : Basis ι R M
h : Function.Bijective ⇑(algebraMap R A)
m : M
⊢ (algebraMapCoeffs A b h).repr m = Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)

Tactic:
rfl

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (single i j 1) M
hki : k ≠ i
⊢ M k i = 0

Tactic:
have := ext_iff.mpr hM k j

Goal state after:
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (single i j 1) M
hki : k ≠ i
this : (single i j 1 * M) k j = (M * single i j 1) k j
⊢ M k i = 0
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inr.inl.inl
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i : n
⊢ M i i = M i i

Tactic:
rfl

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
x : A
ij : ι' × ι
⊢ (b.repr ((c.repr x) ((Equiv.prodComm ι ι').symm ij).2)) ((Equiv.prodComm ι ι').symm ij).1 =
    (b.repr ((c.repr x) ij.1)) ij.2

Tactic:
rfl

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 ((Equiv.prodComm ι ι').symm ij).1 • c ((Equiv.prodComm ι ι').symm ij).2 = b ij.2 • c ij.1

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ f : C →ₐ[A] D
x✝ : C
⊢ (AlgHom.restrictScalars A (AlgHom.extendScalars B f)) x✝ = f x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f : C →ₐ[A] D
g : C → D
map_one'✝¹ : g 1 = 1
map_mul'✝¹ :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one'✝¹ }.toFun (x * y) =
      { toFun := g, map_one' := map_one'✝¹ }.toFun x * { toFun := g, map_one' := map_one'✝¹ }.toFun y
map_zero'✝¹ : (↑{ toFun := g, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun x +
        (↑{ toFun := g, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun y
map_one'✝ : (fun x ↦ g ((algebraMap B C) x)) 1 = 1
map_mul'✝ :
  ∀ (x y : B),
    { toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝ }.toFun x *
        { toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝ }.toFun y
map_zero'✝ : (↑{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun 0 = 0
map_add'✝ :
  ∀ (x y : B),
    (↑{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun (x + y) =
      (↑{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun x +
        (↑{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun y
commutes'✝ :
  ∀ (r : A),
    (↑↑{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝,
                map_add' := map_add'✝ }).toFun
        ((algebraMap A B) r) =
      (algebraMap A D) r
hg :
  ∀ (r : B),
    (↑↑{ toFun := g, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
                map_add' := map_add'✝¹ }).toFun
        ((algebraMap B C) r) =
      (algebraMap B D) r
⊢ (fun f ↦ ⟨AlgHom.domRestrict B f, AlgHom.extendScalars B f⟩)
      ((fun fg ↦
          let x := fg.fst.toAlgebra;
          AlgHom.restrictScalars A fg.snd)
        ⟨{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝,
            map_zero' := map_zero'✝, map_add' := map_add'✝, commutes' := commutes'✝ },
          { toFun := g, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
            map_add' := map_add'✝¹, commutes' := hg }⟩) =
    ⟨{ toFun := fun x ↦ g ((algebraMap B C) x), map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝,
        map_add' := map_add'✝, commutes' := commutes'✝ },
      { toFun := g, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
        commutes' := hg }⟩

Tactic:
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 * if x = a then 1 else 0

Tactic:
by_cases hx : x = a

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ count x s = s.card * if x = a then 1 else 0

case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
⊢ count x s = s.card * if x = a then 1 else 0
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: case mk
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
i : ι
val✝ : α
property✝ : val✝ ∈ iUnion S
hi : ↑⟨val✝, property✝⟩ ∈ S i
⊢ ⟨val✝, property✝⟩ = inclusion ⋯ ⟨↑⟨val✝, property✝⟩, hi⟩

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_3
s : Finset ι
n : ℕ
⊢ n • ∑ x ∈ s, {x} = n • s.val

Tactic:
sum_multiset_singleton

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ n • (Multiset.mapAddMonoidHom g) {a} + toMultiset (mapDomain g f) = n • {g a} + toMultiset (mapDomain g f)

Tactic:
rfl

Goal state after: