mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)
⊢ P a

Tactic:
simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime] at h₃

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Irreducible p → P a → P (p * a)
⊢ P a
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
this : generator S ∈ R ∙ generator S
⊢ S = R ∙ generator S

Tactic:
exact span_singleton_generator S |>.symm

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

Goal state before:
pp: case neg
α : 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (d * a) * a ∣ c * d * a

Tactic:
mul_dvd_mul_iff_right h_1.1

Goal state after:
case neg
α : 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (d * a) ∣ c * d
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
⊢ normalize (Classical.choose ⋯) ∣ a

Tactic:
have h0 : lcm a b ≠ 0 := lcm_ne_zero_iff.mpr ⟨h, h_1⟩

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ normalize (Classical.choose ⋯) ∣ a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
⊢ normalize (Classical.choose ⋯) ∣ b

Tactic:
have h0 : lcm a b ≠ 0 := lcm_ne_zero_iff.mpr ⟨h, h_1⟩

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ normalize (Classical.choose ⋯) ∣ b
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (d * a) * a ∣ c * d * a

Tactic:
mul_dvd_mul_iff_right h_1.1

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (d * a) ∣ c * d
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ IsUnit (gcd x y) ↔ IsCoprime x y

Tactic:
rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]

Goal state after:
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 → α
⊢ (diagonal d).map f = diagonal fun m ↦ f (d m)

Tactic:
by
  ext
  simp only [diagonal_apply, map_apply]
  split_ifs <;> simp [h]

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

Goal state before:
pp: case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ⨆ ι, #↑↑ι ≤ #ι

Tactic:
apply ciSup_le'
    rintro ⟨s, li⟩
    apply linearIndependent_le_basis v _ li

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
inst✝ : Free R M
⊢ 0 < Module.rank R M ↔ Nontrivial M

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ rank_pos_of_free⟩

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
h : 0 < Module.rank R M
⊢ Nontrivial M
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ (M - M') * N = M * N - M' * N

Tactic:
sub_eq_add_neg,

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ (M + -M') * N = M * N - M' * N
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N N' : Matrix n o α
⊢ M * (N - N') = M * N - M * N'

Tactic:
sub_eq_add_neg,

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N N' : Matrix n o α
⊢ M * (N + -N') = M * N - M * N'
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
⊢ ∀ m ∈ { toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } I,
    ∀ n ∈ M, m * n ∈ I • M

Tactic:
by
    rintro _ ⟨r, hr, rfl⟩ a ha; rw [Algebra.linearMap_apply, ← Algebra.smul_def]
    exact Submodule.smul_mem_smul hr ha

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

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

Tactic:
← lift_umax

Goal state after:
case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)
Module: Mathlib.SetTheory.Cardinal.Finsupp

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

Tactic:
← lift_umax

Goal state after:
case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT' : T = iUnion S
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
op : ↑T → ↑T → ↑T
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
x y : ↑T
⊢ iUnionLift S f hf T ⋯ (op x y) = opβ (iUnionLift S f hf T ⋯ x) (iUnionLift S f hf T ⋯ y)

Tactic:
by
  subst hT'
  obtain ⟨i, hi⟩ := Set.mem_iUnion.1 x.prop
  obtain ⟨j, hj⟩ := Set.mem_iUnion.1 y.prop
  rcases dir i j with ⟨k, hik, hjk⟩
  rw [iUnionLift_of_mem x (hik hi), iUnionLift_of_mem y (hjk hj), ← h k]
  have hx : x = Set.inclusion (Set.subset_iUnion S k) ⟨x, hik hi⟩ := by
    cases x
    rfl
  have hy : y = Set.inclusion (Set.subset_iUnion S k) ⟨y, hjk hj⟩ := by
    cases y
    rfl
  have hxy : (Set.inclusion (Set.subset_iUnion S k) (opi k ⟨x, hik hi⟩ ⟨y, hjk hj⟩) : α) ∈ S k :=
    (opi k ⟨x, hik hi⟩ ⟨y, hjk hj⟩).prop
  conv_lhs => rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]

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

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

Tactic:
exact zero_le

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

Goal state before:
pp: case neg
R : Type u
inst✝¹¹ : Semiring R
inst✝¹⁰ : StrongRankCondition R
S : Type u_2
T : Type u_3
inst✝⁹ : Semiring S
inst✝⁸ : Semiring T
inst✝⁷ : Module R T
inst✝⁶ : Module S T
inst✝⁵ : Module R S
inst✝⁴ : IsScalarTower R S T
inst✝³ : IsScalarTower S T T
inst✝² : FaithfulSMul S T
inst✝¹ : Module.Finite S T
inst✝ : Free R S
H : ¬Module.Finite R S
⊢ 0 ≤ finrank R T

Tactic:
exact zero_le

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) ↔ Nonempty (R ≃ₗ[R] S)

Tactic:
exact ⟨fun ⟨e⟩ ↦ ⟨e⟩, fun ⟨e⟩ ↦
    ⟨.ofBijective (Algebra.ofId R S) (bijective_algebraMap_of_linearEquiv e)⟩⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : NonUnitalSubalgebra R A
h1 : 1 ∈ S
⊢ (S.toSubalgebra h1).toNonUnitalSubalgebra = S

Tactic:
by
  cases S; rfl

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:
← one_mul r

Goal state after:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (1 * r)) = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₂ : Type v₂
inst✝⁶ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n : ⨁ (i : ι₂), M₂ i
i : ι₂
⊢ ((directSumRight R S M₁' M₂) (m ⊗ₜ[R] n)) i = m ⊗ₜ[R] n i

Tactic:
suffices (DirectSum.component S ι₂ _ i).restrictScalars R ∘ₗ
      (directSumRight R S M₁' M₂).toLinearMap.restrictScalars R ∘ₗ
        (TensorProduct.mk R M₁' (⨁ i, M₂ i) m) =
          (TensorProduct.mk R M₁' (M₂ i) m) ∘ₗ (DirectSum.component R ι₂ M₂ i) by
    simpa using! LinearMap.congr_fun this n

Goal state after:
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₂ : Type v₂
inst✝⁶ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n : ⨁ (i : ι₂), M₂ i
i : ι₂
⊢ ↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) i) ∘ₗ ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m =
    (mk R M₁' (M₂ i)) m ∘ₗ component R ι₂ M₂ i
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * z)

Tactic:
nth_rewrite 2 [← hz]

Goal state after:
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * star z)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : Monoid R
inst✝³ : StarMul R
inst✝² : Star A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
⊢ IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x

Tactic:
by
  refine ⟨fun hrx ↦ ?_, .smul hr⟩
  lift r to Rˣ using hu
  rw [← inv_smul_smul r x]
  replace hr : IsSelfAdjoint r := Units.ext hr.star_eq
  exact hr.inv.smul hrx

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
M : Matrix n n α
d : ℕ
⊢ M = (↑d).map star ↔ M = ↑d

Tactic:
map_natCast_star

Goal state after:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
M : Matrix n n α
d : ℕ
⊢ M = ↑d ↔ M = ↑d
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
⊢ fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A + A') (B + B') (C + C') (D + D')

Tactic:
ext i j; rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁵ : CommSemiring R
inst✝²⁴ : Semiring A
inst✝²³ : Semiring B
inst✝²² : Algebra R A
inst✝²¹ : Algebra R B
inst✝²⁰ : AddCommMonoid M
inst✝¹⁹ : Module R M
inst✝¹⁸ : Module A M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
inst✝¹² : Module A P
inst✝¹¹ : IsScalarTower R A P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R Q
inst✝⁸ : AddCommMonoid P'
inst✝⁷ : Module R P'
inst✝⁶ : Module A P'
inst✝⁵ : Module B P'
inst✝⁴ : IsScalarTower R A P'
inst✝³ : IsScalarTower R B P'
inst✝² : SMulCommClass A B P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
f : M →ₗ[A] N →ₗ[R] P
c : A
x : M
y : N
⊢ (TensorProduct.lift (↑R f) ∘ₗ (Algebra.lsmul R R (M ⊗[R] N)) c) (x ⊗ₜ[R] y) =
    ((Algebra.lsmul R R P) c ∘ₗ TensorProduct.lift (↑R f)) (x ⊗ₜ[R] y)

Tactic:
simp only [comp_apply, Algebra.lsmul_coe, smul_tmul', lift.tmul,
              coe_restrictScalars, f.map_smul, smul_apply]

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

Goal state before:
pp: ι : 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
x : O
hx : x ∈ N'
⊢ x ∈ M'

Tactic:
simp only [N', mem_map, LinearMap.mem_ker] at hx ⊢

Goal state after:
ι : 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
x : O
hx : ∃ y, (ϕ ∘ₗ inclusion N_le_M) y = 0 ∧ N.subtype y = x
⊢ x ∈ M'
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_2.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'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
z : O
zM : z ∈ M
⊢ M.subtype ⟨z, zM⟩ - ϕ ⟨z, zM⟩ • M.subtype ⟨y', y'M⟩ = z + -ϕ ⟨z, zM⟩ • y'

Tactic:
sub_eq_add_neg,

Goal state after:
case neg.intro.refine_2.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'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
z : O
zM : z ∈ M
⊢ M.subtype ⟨z, zM⟩ + -(ϕ ⟨z, zM⟩ • M.subtype ⟨y', y'M⟩) = z + -ϕ ⟨z, zM⟩ • y'
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: A : Type u_3
inst✝ : Semiring A
⊢ (∀ (n : ℕ), IsDedekindFiniteMonoid (End A (Fin n → A))ᵐᵒᵖ) ↔ ∀ (n : ℕ), IsDedekindFiniteMonoid (End A (Fin n → A))

Tactic:
MulOpposite.isDedekindFiniteMonoid_iff

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx : z * (algebraMap ℤ ℚ) ↑(x1, x2).2 = (algebraMap ℤ ℚ) (x1, x2).1
hx2 : ↑x2 < 0
⊢ z * (algebraMap ℤ ℚ) ↑(-x1, ⟨-↑x2, ⋯⟩).2 = (algebraMap ℤ ℚ) (-x1, ⟨-↑x2, ⋯⟩).1

Tactic:
simpa using hx

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set A
t : Set B
hS : adjoin R s = ⊤
this : adjoin R (⇑(algebraMap A B) '' s) = (IsScalarTower.toAlgHom R A B).range
⊢ Subalgebra.restrictScalars R (adjoin A t) = adjoin R (⇑(algebraMap A B) '' s ∪ t)

Tactic:
adjoin_union_eq_adjoin_adjoin,

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set A
t : Set B
hS : adjoin R s = ⊤
this : adjoin R (⇑(algebraMap A B) '' s) = (IsScalarTower.toAlgHom R A B).range
⊢ Subalgebra.restrictScalars R (adjoin A t) =
    Subalgebra.restrictScalars R (adjoin (↥(adjoin R (⇑(algebraMap A B) '' s))) t)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Submonoid R
a c : R
b d : ↥M
⊢ mk a b - mk c d = mk (↑d * a - ↑b * c) (b * d)

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
M : Submonoid R
a c : R
b d : ↥M
⊢ mk a b + -mk c d = mk (↑d * a - ↑b * c) (b * d)