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

Goal state before:
pp: case refine_1
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.head = RelSeries.head s

Tactic:
RelSeries.head,

Goal state after:
case refine_1
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.toFun 0 = RelSeries.head s
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case refine_1
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.toFun 0 = RelSeries.head s

Tactic:
RelSeries.head,

Goal state after:
case refine_1
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.toFun 0 = s.toFun 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ y, ⨆ (_ : y < ⊤), height y + 1 = (⨆ a, height a) + 1

Tactic:
WithTop.lt_top_iff_ne_top

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ y, ⨆ (_ : y ≠ ⊤), height y + 1 = (⨆ a, height a) + 1
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
m : M
α : Type u_22
s : Finset α
n : α → N
⊢ m ⊗ₜ[R] ∑ a ∈ s, n a = ∑ a ∈ s, m ⊗ₜ[R] n a

Tactic:
induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, tmul_add, ih]

Goal state after:
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ S ≤ R⁰ ↔ ∀ (s : ↥S), IsRegular ↑s

Tactic:
nonZeroDivisors,

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ S ≤ nonZeroDivisorsLeft R ⊓ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRegular ↑s
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsRelPrime x (y + x * z)
⊢ IsRelPrime x y

Tactic:
rw [isRelPrime_comm] at h ⊢

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsRelPrime (y + x * z) x
⊢ IsRelPrime y x
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + z * x)

Tactic:
by
  rw [isCoprime_comm]
  exact h.symm.add_mul_right_left z

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

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
⊢ 1 • N = N

Tactic:
refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_
  · obtain ⟨r, rfl⟩ := hr
    rw [LinearMap.toSpanSingleton_apply, smul_one_smul]; exact N.smul_mem r hm
  · rw [← one_smul A m]; exact smul_mem_smul (one_le.mp le_rfl) hm

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid

Tactic:
obtain rfl | hn := Decidable.eq_or_ne n 0
  · rw [Submodule.pow_zero, pow_zero]
    exact le_one_toAddSubmonoid
  · exact (pow_toAddSubmonoid M hn).ge

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

Goal state before:
pp: case h.zero
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
p : n + 1 ≤ 0
⊢ f 0 = ⊥

Tactic:
cases p

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
m : ℕ
f' : (Fin m → R) →ₗ[R] M
hf' : Surjective ⇑f'
f : (Fin m →₀ Shrink.{v, u} R) →ₗ[R] M :=
  f' ∘ₗ ↑(Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) ≪≫ₗ Finsupp.linearEquivFunOnFinite R R (Fin m))
⊢ ∃ P x x_1, ∃ (_ : Free R P) (_ : Module.Finite R P), ∃ f, Surjective ⇑f

Tactic:
use (Fin m →₀ Shrink.{v, u} R), inferInstance, inferInstance, inferInstance, inferInstance, f

Goal state after:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
m : ℕ
f' : (Fin m → R) →ₗ[R] M
hf' : Surjective ⇑f'
f : (Fin m →₀ Shrink.{v, u} R) →ₗ[R] M := ⋯
⊢ Surjective ⇑f
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ J ⊔ comap f ⊥ = J

Tactic:
sup_eq_left

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f ⊥ ≤ J
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
apply eq_div_of_mul_eq_right h1

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ y * (x / y + z) = x + y * z
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
apply eq_div_of_mul_eq_right h1

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ y * (x / y - z) = x - y * z
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
apply eq_div_of_mul_eq_right h1

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ z * (x + y / z) = z * x + y
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
apply eq_div_of_mul_eq_right h1

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ z * (x - y / z) = z * x - y
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
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
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
⊢ y ∈ j

Tactic:
obtain ⟨x, hx⟩ := (mem_map_iff_of_surjective f hf).1 hy

Goal state after:
case refine_1
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
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ f x = y
⊢ y ∈ j
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, ?_⟩

Goal state after:
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
⊢ I = ⊤ ∨ n = 0 → I ^ n = ⊤
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inl
z : ℤ
h✝ : 0 ≤ z
⊢ |z| = normalize z

Tactic:
simp [abs_of_nonneg, abs_of_nonpos, normalize_of_nonneg, normalize_of_nonpos, *]

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

Goal state before:
pp: case inr
z : ℤ
h✝ : z ≤ 0
⊢ |z| = normalize z

Tactic:
simp [abs_of_nonneg, abs_of_nonpos, normalize_of_nonneg, normalize_of_nonpos, *]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ ∅, x i ∈ I i) → ∏ i ∈ ∅, x i ∈ ∏ i ∈ ∅, I i

Tactic:
grind [Submodule.mem_top]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ normalize (s.gcd f) = s.gcd f

Tactic:
simp [gcd_def]

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

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

Tactic:
hd₁,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd a b ∣ 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf✝ : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
⊢ (factors a).card = 1

Tactic:
rw [hf, card_cons, add_eq_right, card_eq_zero, eq_zero_iff_forall_notMem]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf✝ : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
⊢ ∀ (a : α), a ∉ f
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
P : Ideal R
hp : P.IsPrime
⊢ Multiset.prod 0 ≤ P ↔ ∃ I ∈ 0, I ≤ P

Tactic:
by simp [hp.ne_top]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : a = 0 ∨ b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
· rcases h with (rfl | rfl) <;>
      simp +contextual only [iff_def, lcm_zero_left, lcm_zero_right,
        zero_dvd_iff, dvd_zero, and_true, imp_true_iff]

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b = gcd a c

Tactic:
apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)

Goal state after:
case hab
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b ∣ gcd a c

case hba
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ gcd a b
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case inr
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
hs : range ⇑v ⊆ ⋃ j, S' j
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
refine le_of_not_gt fun IJ => ?_

Goal state after:
case inr
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
hs : range ⇑v ⊆ ⋃ j, S' j
IJ : #↑J < #↑(range ⇑v)
⊢ False
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ j✝ : n
⊢ f (if i✝ = j✝ then 1 else 0) = if i✝ = j✝ then 1 else 0

Tactic:
split_ifs <;> simp [h₀, h₁]

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
inst✝ : Fintype ι
h : Basis ι R M
⊢ Module.rank R M = ↑(Fintype.card ι)

Tactic:
by
  classical
  have := nontrivial_of_invariantBasisNumber R
  rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∈ t
⊢ ∃ i ∈ insert a t, I ≤ f i

Tactic:
obtain ⟨u, hbu, rfl⟩ : ∃ u, b ∉ u ∧ insert b u = t :=
          ⟨t.erase b, Finset.notMem_erase b t, Finset.insert_erase hbt⟩
        have hp' : ∀ i ∈ u, IsPrime (f i) := by
          intro i hiu
          refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_ <;>
              rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h
        rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]

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

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
⊢ ∑ i, single i i (f i) = diagonal f

Tactic:
by
  ext j k
  rw [sum_apply, diagonal_apply, Finset.sum_eq_single j] <;> simp +contextual [single]

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

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✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x✝ : m
⊢ (0 *ᵥ v) x✝ = 0 x✝

Tactic:
simp [mulVec]

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 n
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ 0) x✝ = 0 x✝

Tactic:
simp [mulVec]

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 n
v : n → α
x✝ : m
⊢ (0 *ᵥ v) x✝ = 0 x✝

Tactic:
simp [mulVec]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst✝¹¹ : DecidableEq m
inst✝¹⁰ : DecidableEq n
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : Module S β
inst✝ : SMulCommClass R S β
f : m → n → α →ₗ[R] β
i : m
j : n
a : α
⊢ ((liftLinear S) f) (single i j a) = (f i j) a

Tactic:
dsimp [liftLinear, -LinearMap.lsum_apply, LinearEquiv.congrLeft, LinearEquiv.piCongrRight]

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst✝¹¹ : DecidableEq m
inst✝¹⁰ : DecidableEq n
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : Module S β
inst✝ : SMulCommClass R S β
f : m → n → α →ₗ[R] β
i : m
j : n
a : α
⊢ ((LinearMap.lsum R (fun i ↦ n → α) S) fun i ↦ (LinearMap.lsum R (fun a ↦ α) S) (f i)) (of.symm (single i j a)) =
    (f i j) a
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
u : m → α
v w : n → α
i : m
⊢ (vecMulVec u v *ᵥ w) i = (MulOpposite.op (v ⬝ᵥ w) • u) i

Tactic:
simp [mulVec, dotProduct, vecMulVec, Finset.mul_sum, mul_assoc]

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

Goal state before:
pp: 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
⊢ M = A.submatrix id ⇑e₁

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

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

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

Tactic:
simp only [A, 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 : α →₀ ℕ
⊢ (toMultiset f).toFinset = f.support

Tactic:
by
  refine f.induction ?_ ?_
  · rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]
  · intro a n f ha hn ih
    rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq,
      support_single _ hn, Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]
    refine Disjoint.mono_left support_single_subset ?_
    rwa [Finset.disjoint_singleton_left]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Free R S
⊢ Nonempty (R ≃ₐ[R] S) ↔ finrank R S = 1

Tactic:
by
  rw [← nonempty_linearEquiv_iff_finrank_eq_one]
  exact ⟨fun ⟨e⟩ ↦ ⟨e⟩, fun ⟨e⟩ ↦
    ⟨.ofBijective (Algebra.ofId R S) (bijective_algebraMap_of_linearEquiv e)⟩⟩

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
⊢ ∃! c, u = c • LinearMap.id

Tactic:
suffices u = c • LinearMap.id by
    use c
    simp only [this, true_and]
    intro d hcd
    rw [LinearMap.ext_iff] at hcd
    simpa using (LinearEquiv.congr_arg (e := e.symm) (hcd (e 1))).symm

Goal state after:
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
⊢ u = c • LinearMap.id
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

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
f : A →ₐ[R] B
S : Subalgebra R B
h : S ≤ f.range
⊢ map f (comap f S) = S

Tactic:
by
  simpa only [inf_of_le_left h] using map_comap_eq f S

Goal state after:
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 : S}, a ∈ {x | ∃ m ∈ M, m * x ∈ s} → b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a * b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
intro a b ⟨m, hm, ha⟩ ⟨n, hn, hb⟩
    refine ⟨_, mul_mem hm hn, mul_mul_mul_comm m n a b ▸ mul_mem ha hb⟩

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

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
p q : Subalgebra R A
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
cases p

Goal state after:
case mk
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
q : Subalgebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
h : (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ } = (fun s ↦ s.carrier) q
⊢ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ } = q
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
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ (x + y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ x +
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ y

Tactic:
dsimp
          apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
          all_goals simp

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

Goal state before:
pp: R : Type u
S : Type v
f : R → S
inst✝¹ : Star R
inst✝ : InvolutiveStar S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
r : R
⊢ f (Star.star (Star.star r)) = f r

Tactic:
rw [star, star, star_star]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : Mul α
inst✝ : StarMul α
w : m → α
v : n → α
⊢ (vecMulVec w v).map star = (vecMulVec (star v) (star w))ᵀ

Tactic:
rw [← conjTranspose_vecMulVec]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : Mul α
inst✝ : StarMul α
w : m → α
v : n → α
⊢ (vecMulVec w v).map star = (vecMulVec w v)ᴴᵀ
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: case fst.inl
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι
⊢ ((b.prod b') (Sum.inl val✝)).1 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inl val✝)).1

Tactic:
simp only [prod_apply_inl_fst, Sum.elim_inl, LinearMap.inl_apply, prod_apply_inr_fst,
      Sum.elim_inr, LinearMap.inr_apply, prod_apply_inl_snd, prod_apply_inr_snd, Function.comp]

Goal state after: