mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case e'_2
α✝ : 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
a✝ : Nontrivial α
⊢ 1 * ↑(Exists.choose ⋯) = ↑(if 1 = 0 then 1 else Exists.choose ⋯)

Tactic:
simp [out_one]

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

Goal state before:
pp: case e'_3
α✝ : 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
a✝ : Nontrivial α
⊢ out (Associates.mk 1) = ↑1

Tactic:
simp [out_one]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ normalize 0 = 0

Tactic:
by simp [normalize]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ normalize 1 = 1

Tactic:
by simp [normalize]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
⊢ normalize ↑u = 1

Tactic:
by simp [normalize]

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

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
hi : (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd (GCDMonoid.gcd a (s.gcd f)) (f b) = GCDMonoid.gcd a (GCDMonoid.gcd (g b) (s.gcd g))

Tactic:
hi fun x hx ↦ h _ (mem_insert_of_mem hx),

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s✝ : Finset β
f g : β → α
a : α
b : β
s : Finset β
a✝ : b ∉ s
hi : (∀ x ∈ s, a ∣ f x - g x) → GCDMonoid.gcd a (s.gcd f) = GCDMonoid.gcd a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ GCDMonoid.gcd (GCDMonoid.gcd a (s.gcd g)) (f b) = GCDMonoid.gcd a (GCDMonoid.gcd (g b) (s.gcd g))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : q ∈ span {x}
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : g ∈ span {y}
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ p * (f + d * y) + (c * x * f + c * d * (x * y)) ∈ m

Tactic:
refine
                    m.add_mem (m.mul_mem_right _ hpm)
                    (m.add_mem (m.mul_mem_left _ hfm) (m.mul_mem_left _ hxym))

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
I : Ideal R
this : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h✝ : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h : I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
x✝ : ∃ i ∈ s, I ≤ f i
i : ι
his : i ∈ s
hi : I ≤ f i
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)

Tactic:
refine Set.Subset.trans hi <| Set.Subset.trans ?_ Set.subset_union_right

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
I : Ideal R
this : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h✝ : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
h : I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
x✝ : ∃ i ∈ s, I ≤ f i
i : ι
his : i ∈ s
hi : I ≤ f i
⊢ ↑(f i) ⊆ ⋃ i ∈ ↑s, ↑(f i)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
hgcd : gcd = gcd
⊢ g₁ = g₂

Tactic:
have hlcm : g₁.lcm = g₂.lcm := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [lcm_dvd, dvd_lcm_left, dvd_lcm_right]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
hgcd : gcd = gcd
hlcm : lcm = lcm
⊢ g₁ = g₂
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case hab
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
⊢ gcd a b ∣ c

Tactic:
rcases gcd_dvd_right a b with ⟨e, he⟩

Goal state after:
case hab
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
⊢ gcd a b ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : 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
con : lcm a b = 0
h : lcm a b ∣ a * b
⊢ False

Tactic:
con,

Goal state after:
α : 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
con : lcm a b = 0
h : 0 ∣ a * b
⊢ False
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : 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 c : α
ac : a ∣ c
ab : a ∣ b
h✝ : ¬c = 0
h_1 : ¬b = 0
con : lcm c b = 0
h : lcm c b ∣ c * b
⊢ False

Tactic:
con,

Goal state after:
α : 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 c : α
ac : a ∣ c
ab : a ∣ b
h✝ : ¬c = 0
h_1 : ¬b = 0
con : lcm c b = 0
h : 0 ∣ c * b
⊢ False
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
⊢ ∀ (a b : Associates α), Associated (Quotient.map₂ gcd ⋯ a b * Quotient.map₂ lcm ⋯ a b) (a * b)

Tactic:
by
    rintro ⟨a⟩ ⟨b⟩
    rw [associated_iff_eq]
    exact Quotient.sound <| gcd_mul_lcm _ _

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 w
b : Finset ι
h : Basis (↥b) R M
⊢ finrank R M = b.card

Tactic:
rw [finrank_eq_card_basis h, Fintype.card_coe]

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

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

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

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

Goal state before:
pp: case neg
m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : ¬a j = 0
⊢ (fun k ↦ if k = i then a j else if k = j then -a i else 0) ≠ 0 ∧
    (fun k ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0

Tactic:
refine ⟨Function.ne_iff.mpr ⟨i, by simp [h2]⟩, ?_⟩

Goal state after:
case neg
m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : ¬a j = 0
⊢ (fun k ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
⊢ (single i j r).submatrix ⇑f ⇑g = single (f.symm i) (g.symm j) r

Tactic:
ext i' j'

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
i' : l
j' : m
⊢ (single i j r).submatrix (⇑f) (⇑g) i' j' = single (f.symm i) (g.symm j) r i' j'
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
⊢ ∀ (i j : n), 0 ≤ (A ^ (m + 1)) i j

Tactic:
| succ m ih =>

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
⊢ 0 ᵥ* A = 0

Tactic:
by
  ext
  simp [vecMul]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
v : m → α
⊢ v ᵥ* 0 = 0

Tactic:
by
  ext
  simp [vecMul]

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
i : ι
a✝ : i ∈ a.support
⊢ ↑(if h : a i ∈ I then ⟨a i, h⟩ else 0) • v i = a i • v i

Tactic:
rw [dif_pos (ha i)]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
r : R
⊢ Associates.mk (Ideal.span {r}) ≠ 0 ↔ r ≠ 0

Tactic:
rw [Associates.mk_ne_zero, Ideal.zero_eq_bot, Ne, Ideal.span_singleton_eq_bot]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
⊢ -v ᵥ* -A = v ᵥ* A

Tactic:
vecMul_neg,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
⊢ -(-v ᵥ* A) = v ᵥ* A
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N' : Type v'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
a✝ : Nontrivial M
this : Nontrivial R
w✝ : Set M
B : Basis (↑w✝) R M
cnd : Nonempty (↑w✝ ↪ ι)
⊢ ∃ f, Injective ⇑f

Tactic:
rcases cnd with ⟨i, hi⟩

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N' : Type v'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
a✝ : Nontrivial M
this : Nontrivial R
w✝ : Set M
B : Basis (↑w✝) R M
i : ↑w✝ → ι
hi : Injective i
⊢ ∃ f, Injective ⇑f
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
inst✝ : Nontrivial R
⊢ Nontrivial (TwoSidedIdeal R)

Tactic:
obtain ⟨I, J, h⟩ : Nontrivial (RingCon R) := inferInstance
  exact ⟨⟨I⟩, ⟨J⟩, by contrapose h; aesop⟩

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I ≤ { ringCon := I.ringCon ⊔ J.ringCon }

Tactic:
rw [ringCon_le_iff]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ J ≤ { ringCon := I.ringCon ⊔ J.ringCon }

Tactic:
rw [ringCon_le_iff]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ J.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon } ≤ I

Tactic:
rw [ringCon_le_iff]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon }.ringCon ≤ I.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon } ≤ J

Tactic:
rw [ringCon_le_iff]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon }.ringCon ≤ J.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x✝ : TwoSidedIdeal R
⊢ x✝ ≤ ⊤

Tactic:
rw [ringCon_le_iff]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x✝ : TwoSidedIdeal R
⊢ x✝.ringCon ≤ ⊤.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x✝ : TwoSidedIdeal R
⊢ ⊥ ≤ x✝

Tactic:
rw [ringCon_le_iff]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x✝ : TwoSidedIdeal R
⊢ ⊥.ringCon ≤ x✝.ringCon
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
motive : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
zero : motive 0
of : ∀ (i : ι) (x : β i), motive ((DirectSum.of β i) x)
add : ∀ (x y : ⨁ (i : ι), β i), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
apply DFinsupp.induction x zero

Goal state after:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
motive : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
zero : motive 0
of : ∀ (i : ι) (x : β i), motive ((DirectSum.of β i) x)
add : ∀ (x y : ⨁ (i : ι), β i), motive x → motive y → motive (x + y)
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → motive f → motive (DFinsupp.single i b + f)
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
motive : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
zero : motive 0
of : ∀ (i : ι) (x : β i), motive ((DirectSum.of β i) x)
add : ∀ (x y : ⨁ (i : ι), β i), motive x → motive y → motive (x + y)
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → motive f → motive (DFinsupp.single i b + f)

Tactic:
intro i b f h1 h2 ih

Goal state after:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
motive : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
zero : motive 0
of : ∀ (i : ι) (x : β i), motive ((DirectSum.of β i) x)
add : ∀ (x y : ⨁ (i : ι), β i), motive x → motive y → motive (x + y)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
ih : motive f
⊢ motive (DFinsupp.single i b + f)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ n * m * (a + b) ∈ s

Tactic:
rw [mul_add, mul_assoc, mul_comm n m, mul_assoc]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ n * (m * a) + m * (n * b) ∈ s
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ (∃ s, Function.LeftInverse ⇑(linearCombination R id) ⇑s) ↔
    ∃ s, ∀ (x : P), (linearCombination R id ∘ₗ s) x = LinearMap.id x

Tactic:
Function.LeftInverse,

Goal state after:
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ (∃ s, ∀ (x : P), (linearCombination R id) (s x) = x) ↔
    ∃ s, ∀ (x : P), (linearCombination R id ∘ₗ s) x = LinearMap.id x
Module: Mathlib.Data.Finite.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Finite (α ⊕ β)

Tactic:
have := Fintype.ofFinite α
  have := Fintype.ofFinite β
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ≥0
x : ↥(selfAdjoint R)
⊢ a • ↑x ∈ selfAdjoint R

Tactic:
NNRat.smul_def

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ≥0
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Ring α
inst✝ : StarRing α
M : Matrix n n α
d : ℤ
⊢ M = (↑d)ᴴ ↔ M = ↑d

Tactic:
conjTranspose_intCast

Goal state after:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Ring α
inst✝ : StarRing α
M : Matrix n n α
d : ℤ
⊢ M = ↑d ↔ M = ↑d
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ ↑((skewAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype) ⟨x, hx⟩) = ↑(LinearMap.id ⟨x, hx⟩)

Tactic:
simp only [LinearMap.comp_apply, Submodule.subtype_apply, skewAdjointPart_apply_coe, hx,
      sub_neg_eq_add, smul_add, invOf_two_smul_add_invOf_two_smul]

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ x = ↑(LinearMap.id ⟨x, hx⟩)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
⊢ (blockDiagonal fun k ↦ diagonal (d k)) = diagonal fun ik ↦ d ik.2 ik.1

Tactic:
ext ⟨i, k⟩ ⟨j, k'⟩

Goal state after:
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ blockDiagonal (fun k ↦ diagonal (d k)) (i, k) (j, k') = diagonal (fun ik ↦ d ik.2 ik.1) (i, k) (j, k')
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
⊢ (blockDiagonal fun k ↦ M k * N k) = blockDiagonal M * blockDiagonal N

Tactic:
ext ⟨i, k⟩ ⟨j, k'⟩

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
⊢ blockDiagonal (fun k ↦ M k * N k) (i, k) (j, k') = (blockDiagonal M * blockDiagonal N) (i, k) (j, k')
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
⊢ A.updateRow i r * B = (A * B).updateRow i (r ᵥ* B)

Tactic:
ext i' j'

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
i' : l
j' : n
⊢ (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
j : n
c : m → α
⊢ A * B.updateCol j c = (A * B).updateCol j (A *ᵥ c)

Tactic:
ext i' j'

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
j : n
c : m → α
i' : l
j' : n
⊢ (A * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
⊢ (blockDiagonal' fun k ↦ diagonal (d k)) = diagonal fun ik ↦ d ik.fst ik.snd

Tactic:
ext ⟨i, k⟩ ⟨j, k'⟩

Goal state after:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ blockDiagonal' (fun k ↦ diagonal (d k)) ⟨i, k⟩ ⟨j, k'⟩ = diagonal (fun ik ↦ d ik.fst ik.snd) ⟨i, k⟩ ⟨j, k'⟩
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
⊢ ∀ {x : K}, x ∈ {x | ∃ (hx : x ∈ closure s), p x hx} → -x ∈ {x | ∃ (hx : x ∈ closure s), p x hx}

Tactic:
rintro _ ⟨_, hx⟩; exact ⟨_, neg _ _ hx⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ (M *ᵥ ⇑(Finsupp.single i 1)) j • v₂ j = M j i • v₂ j

Tactic:
Matrix.mulVec,

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ ((fun j_1 ↦ M j j_1) ⬝ᵥ ⇑(Finsupp.single i 1)) • v₂ j = M j i • v₂ j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toMatrix v₁ v₁) id = 1

Tactic:
LinearMap.toMatrix_id

Goal state after: