mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 + a * a∗ = a∗

Tactic:
by
  have h : 1 + a * a∗ ≤ a∗ := by
    rw [add_le_iff]
    exact ⟨one_le_kstar, mul_kstar_le_kstar⟩
  apply le_antisymm h
  suffices 1 + a * (1 + a * a∗) ≤ 1 + a * a∗ by
    rw [add_le_iff] at this
    nth_rw 1 [← mul_one a∗]
    exact (mul_right_mono this.1).trans (kstar_mul_le_self this.2)
  apply add_le_add_right (mul_right_mono h)

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

Goal state before:
pp: case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ closure S * closure T

Tactic:
rw [closure_le]
    rintro _ ⟨a, ha, b, hb, rfl⟩
    exact mul_mem_mul (subset_closure ha) (subset_closure hb)

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ ¬toInt val i < toInt val j ↔ ¬val i < val j

Tactic:
simpa using toInt_le_toInt val j i

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal
    (Ideal.span ({generator (Ideal.map (RingHom.fst R S) I)} ×ˢ {generator (Ideal.map (RingHom.snd R S) I)}))

Tactic:
Set.singleton_prod_singleton

Goal state after:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal
    (Ideal.span {(generator (Ideal.map (RingHom.fst R S) I), generator (Ideal.map (RingHom.snd R S) I))})
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (map (algebraMap R S) I • N) = I • Submodule.restrictScalars R N

Tactic:
map,

Goal state after:
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (span (⇑(algebraMap R S) '' ↑I) • N) = I • Submodule.restrictScalars R N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
⊢ ∀ (m : Π₀ (i : ι), M i), r • m = 0

Tactic:
intro m; ext i; exact h i _

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
⊢ ∀ (m : (i : ι) → M i), r • m = 0

Tactic:
intro m; ext i; exact h i _

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

Goal state before:
pp: case refine_2
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
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
⊢ ∀ p ∈ A, x ∈ p

Tactic:
intro J hJ

Goal state after:
case refine_2
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
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
J : Submodule R R
hJ : J ∈ A
⊢ x ∈ J
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ Associated (s.gcd fun x ↦ a * f x) (a * s.gcd f)

Tactic:
classical exact s.induction_on (by simp) fun b s hbs h ↦ by
             simpa using .trans (.gcd .rfl h) (gcd_mul_left' ..)

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

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : DivisionMonoid α
inst✝ : SubmonoidClass C α
S : C
u : (↥S)ˣ
⊢ (↑↑u)⁻¹ = ↑↑u⁻¹

Tactic:
exact (map_inv ((subtype <| ofClass S).comp <| Units.coeHom S) u).symm

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
b c : α
⊢ Associated (gcd (0 * b) (0 * c)) (0 * gcd b c)

pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
⊢ Associated (gcd (a * b) (a * c)) (a * gcd b c)

Tactic:
· simp only [zero_mul, gcd_zero_left']

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
⊢ Associated (gcd (a * b) (a * c)) (a * gcd b c)
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
have hm'n' : m' * n' ∣ k := h ▸ gcd_dvd_left _ _

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ m' * n' ∣ gcd k m * gcd k n
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
⊢ WellFounded (Function.onFun (fun x1 x2 ↦ x1 > x2) fun a ↦ span {a})

Tactic:
convert! wellFounded_dvdNotUnit (α := α)

Goal state after:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
⊢ (Function.onFun (fun x1 x2 ↦ x1 > x2) fun a ↦ span {a}) = DvdNotUnit
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
⊢ a * b * ↑(Classical.choose ⋯) = f (Associates.mk a) * (b * ↑(Classical.choose ⋯))

Tactic:
map_mk_unit_aux hinv (a * b),

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
⊢ f (Associates.mk (a * b)) = f (Associates.mk a) * (b * ↑(Classical.choose ⋯))
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inr
α : 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✝ : b = 0
⊢ False

Tactic:
· exact absurd ‹b = 0› h_1

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

Goal state before:
pp: case inr
α : 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✝ : b = 0
⊢ False

Tactic:
· exact absurd ‹b = 0› h_1

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NormalizationMonoid R
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ ∃ x_1, normalize x_1 = x_1 ∧ R ∙ x = span {x_1}

Tactic:
refine ⟨normalize x, normalize_idem x, le_antisymm ?_ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NormalizationMonoid R
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ R ∙ x ≤ span {normalize x}

case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NormalizationMonoid R
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ span {normalize x} ≤ R ∙ x
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
| ∀ (i j : n), (if i = j then d i else 0) ∈ S

Tactic:
intro _ _; rw [ite_mem]

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
i✝ j✝ : n
| (i✝ = j✝ → d i✝ ∈ S) ∧ (¬i✝ = j✝ → 0 ∈ S)
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : AddMonoidWithOne α
⊢ (diagonal fun x ↦ 0) = 0

Tactic:
diagonal_zero

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n
inst✝ : AddMonoidWithOne α
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := ⋯
⊢ LinearIndependent R fun i ↦ f (single i 1)

Tactic:
LinearIndependent

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
⊢ Injective ⇑(linearCombination R fun i ↦ f (single i 1))
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
s : Set M
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R s) = #↑s

Tactic:
rw [← @ofPred_mem_eq _ s, ← Subtype.range_coe_subtype]

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R (range Subtype.val)) = #↑(range Subtype.val)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : MulOneClass α
inst✝ : AddCommMonoid α
v : n → α
⊢ v ⬝ᵥ 1 = ∑ i, v i

Tactic:
by simp [(· ⬝ᵥ ·)]

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : MulOneClass α
inst✝ : AddCommMonoid α
v : n → α
⊢ 1 ⬝ᵥ v = ∑ i, v i

Tactic:
by simp [(· ⬝ᵥ ·)]

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

Goal state before:
pp: case neg.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
hp : ∀ i ∈ ∅, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑∅, ↑(f i)
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ i ∈ ∅, I ≤ f i

Tactic:
rw [Finset.coe_empty, Set.biUnion_empty] at h

Goal state after:
case neg.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
hp : ∀ i ∈ ∅, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ∅
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ i ∈ ∅, I ≤ f i
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
⊢ single i j 0 = 0

Tactic:
by
  unfold single
  ext
  simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
| ∀ (i_1 : m) (j_1 : n), (if i = i_1 ∧ j = j_1 then a else 0) ∈ S

Tactic:
intro _ _; rw [ite_mem]

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
i✝ : m
j✝ : n
| (i = i✝ ∧ j = j✝ → a ∈ S) ∧ (¬(i = i✝ ∧ j = j✝) → 0 ∈ S)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
I : Ideal R
⊢ s • I ≤ Ideal.span s

Tactic:
by
  simp [← Submodule.set_smul_top_eq_span, smul_le_smul_left]

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

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

Tactic:
by
  ext
  apply dotProduct_comm

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

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

Tactic:
by
  ext
  apply dotProduct_comm

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : AddCommMonoid α
inst✝¹ : CommMagma α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n l α
⊢ (M * N)ᵀ = Nᵀ * Mᵀ

Tactic:
by
  ext
  apply dotProduct_comm

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
inhabited_h : Inhabited α
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ ((toFinsupp s).sum fun x ↦ id) = s.card

Tactic:
← Finsupp.card_toMultiset,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ (Finsupp.toMultiset (toFinsupp s)).card = s.card
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i, P i = n
a : α
⊢ Multiset.count a (Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P)) =
    Multiset.count a (Multiset.map (fun a ↦ ↑⟨P, hP⟩ a • {a}) univ.val).sum

Tactic:
Multiset.count_sum

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i, P i = n
a : α
⊢ Multiset.count a (Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P)) =
    (Multiset.map (fun b ↦ Multiset.count a (↑⟨P, hP⟩ b • {b})) univ.val).sum
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (algebraMap R A) r ∈ Set.center A

Tactic:
simp only [Semigroup.mem_center_iff, commutes, forall_const]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
⊢ 0 ∈ {a | ϕ a = ψ a}

Tactic:
by simp only [Set.mem_ofPred_eq, map_zero]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : A →ₙₐ[R] B
⊢ ↑(NonUnitalSubalgebra.map f ⊥) = ↑⊥

Tactic:
by simp [NonUnitalAlgebra.coe_bot, NonUnitalSubalgebra.coe_map]

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

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
x y : (ι →₀ M) ⊗[R] N
hx : ((finsuppLeft R S M N ι) x) i = (rTensor N (Finsupp.lapply i)) x
hy : ((finsuppLeft R S M N ι) y) i = (rTensor N (Finsupp.lapply i)) y
⊢ ((finsuppLeft R S M N ι) (x + y)) i = (rTensor N (Finsupp.lapply i)) (x + y)

Tactic:
simp [map_add, hx, hy]

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

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
x y : M ⊗[R] (ι →₀ N)
hx : ((finsuppRight R S M N ι) x) i = (lTensor M (Finsupp.lapply i)) x
hy : ((finsuppRight R S M N ι) y) i = (lTensor M (Finsupp.lapply i)) y
⊢ ((finsuppRight R S M N ι) (x + y)) i = (lTensor M (Finsupp.lapply i)) (x + y)

Tactic:
simp [map_add, hx, hy]

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

Goal state before:
pp: R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r

Tactic:
nth_rw 1 [← one_mul r]
  exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint (star x * x)

Tactic:
simp only [IsSelfAdjoint, star_mul, star_star]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Mul R
inst✝¹ : StarMul R
x : R
inst✝ : IsStarNormal x
⊢ x * star x = star x * x

Tactic:
star_comm_self'

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : Mul R
inst✝¹ : StarMul R
x : R
inst✝ : IsStarNormal x
⊢ x * star x = x * star x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : StarAddMonoid R
x : R
inst✝ : IsStarNormal x
⊢ star x * x = x * star x

Tactic:
star_comm_self'

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

Goal state before:
pp: n : Type u_3
α : Type v
ι : Type u_6
inst✝ : Nonempty ι
⊢ Function.Injective (replicateRow ι)

Tactic:
by
  inhabit ι
  exact fun _x _y h => funext fun j => congr_fun₂ h default j

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

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Tactic:
· rw [updateRow_ne h, if_neg h]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal 0 i✝ j✝ = 0 i✝ j✝

Tactic:
simp [blockDiagonal_apply]

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

Goal state before:
pp: case inr
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
hj : j' ≠ j
⊢ (A * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'

Tactic:
· simp [mul_apply, hj]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ baseChange A p = span A ↑(map ((TensorProduct.mk R A M) 1) p)

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ baseChange A p ≤ span A ↑(map ((TensorProduct.mk R A M) 1) p)

case refine_2
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ span A ↑(map ((TensorProduct.mk R A M) 1) p) ≤ baseChange A p
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
x : ↥f.fieldRange
⊢ ↑(f.rangeRestrictFieldEquiv (f.rangeRestrictFieldEquiv.symm x)) = ↑x

Tactic:
RingEquiv.apply_symm_apply

Goal state after:
K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
x : ↥f.fieldRange
⊢ ↑x = ↑x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_7
inst✝ : Unique ι
f : R →ₗ[R] R
i j : ι
⊢ (toMatrix (Basis.singleton ι R) (Basis.singleton ι R)) f i j = f 1

Tactic:
by
  simp [toMatrix, Subsingleton.elim j default]

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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (sc • rb • r₁ + 1 • rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
rw [OreLocalization.expand' (sa • r₂ + ra • r₃) (sa * s₂) (sc * sb)]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((sc * sb) • (sa • r₂ + ra • r₃) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (sc • rb • r₁ + 1 • rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommGroup X
inst✝ : Module R X
n : ℤ
x : OreLocalization S X
⊢ n • x = n • x

Tactic:
let inst := OreLocalization.instModuleOfIsScalarTower (R₀ := ℤ) (R := R) (X := X) (S := S)
  exact congr($(AddCommGroup.uniqueIntModule.2 inst).smul n x)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
h : numeratorHom r₁ = numeratorHom r₂
⊢ r₁ = r₂

Tactic:
rw [numeratorHom_apply, numeratorHom_apply, oreDiv_eq_iff] at h

Goal state after:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
h : ∃ u v, u • r₂ = v • r₁ ∧ ↑u * ↑1 = v * ↑1
⊢ r₁ = r₂
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
hi : i ∉ range ⇑snf.f
c : Fin n →₀ R
hm : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
⊢ (snf.bM.repr ↑⟨c.sum fun i x ↦ x • ↑(snf.bN i), hm⟩) i = 0

Tactic:
replace hi : ∀ j, snf.f j ≠ i := by simpa using hi

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
c : Fin n →₀ R
hm : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hi : ∀ (j : Fin n), snf.f j ≠ i
⊢ (snf.bM.repr ↑⟨c.sum fun i x ↦ x • ↑(snf.bN i), hm⟩) i = 0