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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : x ∈ Module.annihilator R M'
⊢ x ∈ Module.annihilator R M

Tactic:
rw [Module.mem_annihilator] at h ⊢; exact fun m ↦ hf (by rw [map_smul, h, f.map_zero])

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

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

Tactic:
rw [← mul_assoc, ← mul_div_assoc _ (by gcongr), mul_div_cancel_left₀ _ (mul_ne_zero ha hc)]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ 0 ∣ x

Tactic:
← h

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ s.gcd ∣ x
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst✝² : EquivLike F' R S
inst✝¹ : RingEquivClass F' R S
f : F'
I : Ideal R
inst✝ : I.IsPrime
h : map f I = map (↑↑f) I
⊢ (map f I).IsPrime

Tactic:
rw [h, map_comap_of_equiv (RingEquivClass.toRingEquiv f : R ≃+* S)]

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst✝² : EquivLike F' R S
inst✝¹ : RingEquivClass F' R S
f : F'
I : Ideal R
inst✝ : I.IsPrime
h : map f I = map (↑↑f) I
⊢ (comap (↑f).symm I).IsPrime
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
| s

Tactic:
rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
| pmap (fun a x ↦ id a) s ⋯
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
⊢ I ^ n = ⊤ ↔ I = ⊤ ∨ n = 0

Tactic:
refine ⟨fun h ↦ or_iff_not_imp_right.mpr
      fun hn ↦ (eq_top_iff_one _).mpr <| pow_le_self hn <| (eq_top_iff_one _).mp h, ?_⟩
  rintro (h | h)
  · rw [h, top_pow]
  · rw [h, Submodule.pow_zero, one_eq_top]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Fintype ι
I : ι → ℕ
hI : Pairwise fun i j ↦ (I i).Coprime (I j)
⊢ ⨅ i, span {↑(I i)} = span {↑(∏ i, I i)}

Tactic:
iInf_span_singleton,

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Fintype ι
I : ι → ℕ
hI : Pairwise fun i j ↦ (I i).Coprime (I j)
⊢ span {∏ i, ↑(I i)} = span {↑(∏ i, I i)}

R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Fintype ι
I : ι → ℕ
hI : Pairwise fun i j ↦ (I i).Coprime (I j)
⊢ ∀ (i j : ι), i ≠ j → IsCoprime ↑(I i) ↑(I j)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
⊢ (a ::ₘ s).prod ≤ (a ::ₘ s).inf

Tactic:
rw [Multiset.prod_cons, Multiset.inf_cons]

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
⊢ a * s.prod ≤ a ⊓ s.inf
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
⊢ (if 1 = 0 then 1 else Exists.choose ⋯) = 1

Tactic:
nontriviality α; rw [← Units.val_inj]; convert ← (assoc 1).choose_spec <;> simp [out_one]

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

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

Tactic:
← h

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommMonoidWithZero α
x✝ : IsGCDMonoid α
a✝ : GCDMonoid α
⊢ Nonempty (NormalizedGCDMonoid α)

Tactic:
have := Classical.arbitrary (NormalizationMonoid α)

Goal state after:
α : Type u_2
inst✝ : CommMonoidWithZero α
x✝ : IsGCDMonoid α
a✝ : GCDMonoid α
this : NormalizationMonoid α
⊢ Nonempty (NormalizedGCDMonoid α)
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
⊢ (diagonal d).map f i✝ j✝ = diagonal (fun m ↦ f (d m)) i✝ j✝

Tactic:
simp only [diagonal_apply, map_apply]

Goal state after:
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
⊢ f (if i✝ = j✝ then d i✝ else 0) = if i✝ = j✝ then f (d i✝) else 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
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
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
⊢ False

Tactic:
rw [Finset.coe_insert, Set.biUnion_insert] at h

Goal state after:
case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x))
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
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
⊢ False
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
inst✝ : Module.Finite R M
⊢ ↑(finrank R M) = Module.rank R M

Tactic:
rw [Module.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]

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

Goal state before:
pp: R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ finrank S M ≤ finrank R M

Tactic:
rw [finrank, finrank, Cardinal.toNat_le_iff_le_of_lt_aleph0]

Goal state after:
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank S M ≤ Module.rank R M

case hc
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank S M < ℵ₀

case hd
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank R M < ℵ₀
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
⊢ (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w

Tactic:
simp [dotProduct, add_mul, Finset.sum_add_distrib]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
⊢ Pi.single i x ⬝ᵥ v = x * v i

Tactic:
have : ∀ j ≠ i, (Pi.single i x : m → α) j * v j = 0 := fun j hij => by
    simp [Pi.single_eq_of_ne hij]
  convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
⊢ a • M = M * diagonal fun x ↦ a

Tactic:
by
  ext
  simp [mul_comm]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ ↑I
a : A
ha : a ∈ M
⊢ (Algebra.linearMap R A) r * a ∈ I • M

Tactic:
rw [Algebra.linearMap_apply, ← Algebra.smul_def]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ ↑I
a : A
ha : a ∈ M
⊢ r • a ∈ I • M
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
⊢ Module.Finite R M

Tactic:
cases nonempty_fintype ι
  classical
    refine ⟨⟨Finset.univ.image b, ?_⟩⟩
    simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]

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

Goal state before:
pp: case inr.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 j : n
⊢ diagonal (fun x ↦ M i i) j j = M j j

Tactic:
rw [diagonal_apply_eq]

Goal state after:
case inr.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 j : n
⊢ M i i = M j j
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inr.inr
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 j k : n
hkl : j ≠ k
⊢ diagonal (fun x ↦ M i i) j k = M j k

Tactic:
diagonal_apply_ne _ hkl

Goal state after:
case inr.inr
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 j k : n
hkl : j ≠ k
⊢ 0 = M j k
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case intro
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := M.submatrix id ⇑e₁.symm
this : M = A.submatrix id ⇑e₁
⊢ (A * 1).submatrix id e₂ = (A.submatrix id ⇑e₁).submatrix id (⇑e₁.symm ∘ e₂)

Tactic:
simp only [A, Matrix.mul_one, submatrix_submatrix, Function.comp_id, submatrix_id_id,
    Equiv.symm_comp_self]

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

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

Tactic:
toMultiset_apply

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (f.sum fun a n ↦ n • {a}) = f.sum fun x n ↦ Multiset.count a (n • {x})
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ finrank F K * finrank K A = finrank F A

Tactic:
simp_rw [finrank]

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ toNat (Module.rank F K) * toNat (Module.rank K A) = toNat (Module.rank F A)
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
H' : a - b ∈ {x | t₂ x 0}
⊢ t₁ a b

Tactic:
← h

Goal state after:
case refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
H' : a - b ∈ {x | { ringCon := t₁ }.ringCon x 0}
⊢ t₁ a b
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
M : Type u_1
S : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ HasFiniteSupport fun i ↦ ↑(x i)

Tactic:
exact (DFinsupp.support x).finite_toSet.subset (DirectSum.support_subset _ x)

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ adjoin R ⊥ = ⊥

Tactic:
apply GaloisConnection.l_bot

Goal state after:
case gc
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ GaloisConnection (adjoin R) ?u

case u
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ NonUnitalSubalgebra R A → Set A
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
⊢ diagonal (fun i ↦ diagonal fun j ↦ d i j) i₁ i₁ j₁ j₂ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂)

Tactic:
rw [diagonal_apply_eq]

Goal state after:
case inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
⊢ diagonal (fun j ↦ d i₁ j) j₁ j₂ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂)
Module: Mathlib.Algebra.Star.BigOperators

Goal state before:
pp: R : Type u_1
ι : Type u_2
M : Type u_3
inst✝² : Zero M
inst✝¹ : CommMonoid R
inst✝ : StarMul R
s : ι →₀ M
f : ι → M → R
⊢ star (s.prod f) = s.prod fun i m ↦ star f i m

Tactic:
by
  simp [Finsupp.prod]

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

Goal state before:
pp: case inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = diagonal (Function.update v i x) j j

Tactic:
rw [diagonal_apply_eq]

Goal state after:
case inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ (diagonal d).blockDiag k i i = diagonal (fun i ↦ d (i, k)) i i

Tactic:
rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
⊢ ∀ z ∈ N, ∃ c, z + c • y ∈ N'

Tactic:
intro z

Goal state after:
case neg.intro.refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
z : O
⊢ z ∈ N → ∃ c, z + c • y ∈ N'
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
⊢ rd * rb * ↑s₁ = ↑sd * ↑sc * ↑s₃

Tactic:
rw [mul_assoc, ← hb', ← mul_assoc, ← hd, mul_assoc, ← hc, mul_assoc]

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

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
y z : OreLocalization S X
r₁ : X
s₁ : ↥S
⊢ r₁ /ₒ s₁ + y + z = r₁ /ₒ s₁ + (y + z)

Tactic:
induction y with

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ r₁ /ₒ s₁ + r₂ /ₒ s₂ + z = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + z)
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_2.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
⊢ ∀ z ∈ M, ∃ c, z + c • y' ∈ M'

Tactic:
intro z

Goal state after:
case neg.intro.refine_2.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
z : O
⊢ z ∈ M → ∃ c, z + c • y' ∈ M'
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i✝ j✝ : n
⊢ toMatrix' id i✝ j✝ = 1 i✝ j✝

Tactic:
Matrix.one_apply,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i✝ j✝ : n
⊢ toMatrix' id i✝ j✝ = if i✝ = j✝ then 1 else 0