mathlib-initiative/mathlib-tactics huggingface dataset:
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
hIm : I ≤ ⊤
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) ⊤
hrm : r ∉ ⊤.radical
this : ∀ x ∉ ⊤, r ∈ (⊤ ⊔ span {x}).radical
⊢ False

Tactic:
radical_top

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) ⊤
hrm : r ∉ ⊤
this : ∀ x ∉ ⊤, r ∈ (⊤ ⊔ span {x}).radical
⊢ False
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : a = 0
⊢ ∃ d, Associated (d ^ k) a

Tactic:
use 0
    obtain rfl | hk := eq_or_ne k 0
    · simp [ha] at h
    · rw [ha, zero_pow hk]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a b : α
a0 : a = 0
⊢ Associated (gcd a b * 0) (a * b)

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a b : α
a0 : ¬a = 0
⊢ Associated (gcd a b * Classical.choose ⋯) (a * b)

Tactic:
· rw [mul_zero, a0, zero_mul]

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a b : α
a0 : ¬a = 0
⊢ Associated (gcd a b * Classical.choose ⋯) (a * b)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
a0 : a = 0
⊢ Associated (gcd a b * 0) (a * b)

pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
⊢ Associated (gcd a b * normalize (Classical.choose ⋯)) (a * b)

Tactic:
· rw [mul_zero, a0, zero_mul]

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
⊢ Associated (gcd a b * normalize (Classical.choose ⋯)) (a * b)
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ Ideal.span {x, y}

Tactic:
← span_gcd

Goal state after:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ Ideal.span {gcd x y}
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : R ∙ a * b < R ∙ a
hb : IsUnit b
⊢ R ∙ a ≤ R ∙ a * b

Tactic:
rw [Ideal.submodule_span_eq, Ideal.submodule_span_eq,
        Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
⊢ dite P A B i j = if x : P then A x i j else B x i j

Tactic:
by_cases h : P <;> simp [h]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, (∀ (i : m) (j : n), A i j + b i j = 0 i j) ∧ ∀ (i : m) (j : n), b i j + A i j = 0 i j) ↔
    ∃ f, (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0

Tactic:
zero_apply

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, (∀ (i : m) (j : n), A i j + b i j = 0) ∧ ∀ (i : m) (j : n), b i j + A i j = 0) ↔
    ∃ f, (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j : n
d : ℤ
⊢ ↑d i j = if i = j then ↑d else ↑0

Tactic:
Int.cast_zero,

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j : n
d : ℤ
⊢ ↑d i j = if i = j then ↑d else 0
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
inst✝ : Module.Finite R M
⊢ 0 < finrank R M ↔ Nontrivial M

Tactic:
rw [← not_subsingleton_iff_nontrivial, ← iff_not_comm]

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
inst✝ : Module.Finite R M
⊢ Subsingleton M ↔ ¬0 < finrank R M
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

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

Tactic:
rw [finrank, finrank, Cardinal.toNat_le_iff_le_of_lt_aleph0]
  · exact rank_top_le_rank_of_isScalarTower R S M
  · exact lt_of_le_of_lt (rank_top_le_rank_of_isScalarTower R S M) (Module.rank_lt_aleph0 R M)
  · exact Module.rank_lt_aleph0 _ _

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Mul α
inst✝¹ : Zero α
inst✝ : NoZeroDivisors α
a b : n → α
ha : a ≠ 0
hb : b ≠ 0
⊢ vecMulVec a b ≠ 0

Tactic:
by
  intro h
  obtain ⟨i, ha⟩ := Function.ne_iff.mp ha
  obtain ⟨j, hb⟩ := Function.ne_iff.mp hb
  exact mul_ne_zero ha hb congr($h i j)

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 → α
⊢ 0 *ᵥ v = 0

Tactic:
ext
    simp [mulVec]

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

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I J K L : Ideal R
u : (Ideal R)ˣ
⊢ ↑u = 1

Tactic:
rw [isUnit_iff.mp u.isUnit, one_eq_top]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
I : Ideal R
f : M →ₗ[R] N
h : Function.Surjective ⇑f
⊢ comap f (I • ⊤) = comap f (I • f.range)

Tactic:
LinearMap.range_eq_top.mpr h

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
I : Ideal R
f : M →ₗ[R] N
h : Function.Surjective ⇑f
⊢ comap f (I • ⊤) = comap f (I • ⊤)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
z : R
hzs : z ∈ s
hs : s ⊆ ↑{ carrier := {r | ∃ n, ∃ y ∈ I, ∃ z ∈ J, y + z = r ^ n}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
m : ℕ
y : R
hyq : y ∈ I
b : R
hb : b ∈ J
hy : y + b = z ^ m
⊢ ∃ m a b, ∃ (_ : a ∈ I) (_ : b ∈ J), a + b = ↑⟨z, hzs⟩ ^ m

Tactic:
exact ⟨m, y, b, hyq, hb, hy⟩

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

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single i 1 = 0
h' : l = l - k + k
⊢ M ^ l *ᵥ Pi.single i 1 = 0

Tactic:
rw [h', pow_add, ← mulVec_mulVec, h, mulVec_zero]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ (toMultiset 0).prod = prod 0 fun a n ↦ a ^ n

pp: case refine_2
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        ((toMultiset f).prod = f.prod fun a n ↦ a ^ n) →
          (toMultiset (single a b + f)).prod = (single a b + f).prod fun a n ↦ a ^ n

Tactic:
· rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        ((toMultiset f).prod = f.prod fun a n ↦ a ^ n) →
          (toMultiset (single a b + f)).prod = (single a b + f).prod fun a n ↦ a ^ n
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: n : Type u_3
α : Type u_11
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
⊢ 0 ≤ 1 i j

Tactic:
by_cases hi : i = j

Goal state after:
case pos
n : Type u_3
α : Type u_11
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
hi : i = j
⊢ 0 ≤ 1 i j

case neg
n : Type u_3
α : Type u_11
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
hi : ¬i = j
⊢ 0 ≤ 1 i j
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
x : Matrix m n α
s : Finset ι
y : ι → n → α
x✝ : m
⊢ (x *ᵥ ∑ i ∈ s, y i) x✝ = (∑ i ∈ s, x *ᵥ y i) x✝

Tactic:
simp only [mulVec, dotProduct_sum, Finset.sum_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y ↔ x - y ∈ I

Tactic:
rw [mem_iff]
  constructor
  · intro h; convert! I.ringCon.sub h (I.ringCon.refl y); abel
  · intro h; convert! I.ringCon.add h (I.ringCon.refl y) <;> abel

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

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (α i)
inst✝ : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → α i →+ β i
x y : ⨁ (i : ι), α i
⊢ (map f) x = (map f) y ↔ ∀ (i : ι), (f i) (x i) = (f i) (y i)

Tactic:
DirectSum.ext_iff,

Goal state after:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (α i)
inst✝ : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → α i →+ β i
x y : ⨁ (i : ι), α i
⊢ (∀ (i : ι), ((map f) x) i = ((map f) y) i) ↔ ∀ (i : ι), (f i) (x i) = (f i) (y i)
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 : Type u_4
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : Set.EqOn ⇑↑φ ⇑↑ψ ↑S
hT : Set.EqOn ⇑↑φ ⇑↑ψ ↑T
⊢ Set.EqOn ⇑↑φ ⇑↑ψ ↑(S ⊔ T)

Tactic:
← le_equalizer

Goal state after:
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 : Type u_4
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ ψ : F
S T : Subalgebra R A
hS : S ≤ (↑φ).equalizer ↑ψ
hT : T ≤ (↑φ).equalizer ↑ψ
⊢ S ⊔ T ≤ (↑φ).equalizer ↑ψ
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
⊢ IsInternal fun i ↦ Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
by
  refine (isInternal_submodule_iff_iSupIndep_and_iSup_eq_top _).mpr ⟨?_, by simp [iSup_subtype]⟩
  let p := ⨆ i ∈ s, A i
  have hp : ∀ i ∈ s, A i ≤ p := fun i hi ↦ le_biSup A hi
  let e : Submodule R p ≃o Set.Iic p := p.mapIic
  suffices (e ∘ fun i : s ↦ (A i).comap p.subtype) = fun i ↦ ⟨A i, hp i i.property⟩ by
    rw [← iSupIndep_map_orderIso_iff e, this]
    exact .of_coe_Iic_comp h
  ext i m
  change m ∈ ((A i).comap p.subtype).map p.subtype ↔ _
  rw [Submodule.map_comap_subtype, inf_of_le_right (hp i i.property)]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℤ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
by
  simp only [isSelfAdjoint_iff, star_zpow₀, hx.star_eq]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
⊢ Commute (star (a + b)) (a + b)

Tactic:
have := _root_.star_star b ▸ hab.star_star

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ Commute (star (a + b)) (a + b)
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
r : R
x : A
⊢ ⟨⅟2 • (r • x + star (r • x)), ⋯⟩ = (RingHom.id R) r • ⟨⅟2 • (x + star x), ⋯⟩

Tactic:
by
    ext
    simp [← mul_smul, show ⅟2 * r = r * ⅟2 from Commute.invOf_left <| (2 : ℕ).cast_commute r]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
M : Matrix m n α
N : Matrix n l α
⊢ ∀ (i : l) (j : m), (M * N)ᴴ i j = (Nᴴ * Mᴴ) i j

Tactic:
by simp [mul_apply]

Goal state after:
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✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
i : l
r : m → α
j : n
c : m → α
⊢ (updateCol 0 j (0 *ᵥ c)).updateRow i (Function.update 0 j (r ⬝ᵥ c)) = of (Pi.single i (Pi.single j (r ⬝ᵥ c)))

Tactic:
zero_mulVec,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq l
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
i : l
r : m → α
j : n
c : m → α
⊢ (updateCol 0 j 0).updateRow i (Function.update 0 j (r ⬝ᵥ c)) = of (Pi.single i (Pi.single j (r ⬝ᵥ c)))
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ baseChange A (-f) = -baseChange A f

Tactic:
ext
  simp [tmul_neg]

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Defs

Goal state before:
pp: K : Type u
inst✝¹ : DivisionRing K
S : Type u_1
inst✝ : SetLike S K
h : SubfieldClass S K
x : K
s : S
q : ℚ≥0
hx : x ∈ s
⊢ q • x ∈ s

Tactic:
by
  simpa only [NNRat.smul_def] using mul_mem (nnratCast_mem _ _) hx

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
m : Type u_3
inst✝¹ : Fintype m
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ Function.Injective fun v ↦ v ᵥ* A

Tactic:
exact Matrix.vecMul_injective_of_isUnit ha

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
s : Set K
x : K
⊢ x ∈ closure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x

Tactic:
← commClosure_eq_closure

Goal state after:
K : Type u
inst✝ : Field K
s : Set K
x : K
⊢ x ∈ commClosure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ (r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) =
    (r₃ /ₒ s₃) • (sa • r₁ /ₒ (sa * s₁)) + (r₃ /ₒ s₃) • (ra • r₂ /ₒ (sa * s₁))

Tactic:
rw [oreDiv_smul_oreDiv]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
    (r₃ /ₒ s₃) • (sa • r₁ /ₒ (sa * s₁)) + (r₃ /ₒ s₃) • (ra • r₂ /ₒ (sa * s₁))
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
    (r₃ /ₒ s₃) • (sa • r₁ /ₒ (sa * s₁)) + (r₃ /ₒ s₃) • (ra • r₂ /ₒ (sa * s₁))

Tactic:
rw [oreDiv_smul_oreDiv]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
    oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃) + (r₃ /ₒ s₃) • (ra • r₂ /ₒ (sa * s₁))
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
    oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃) + (r₃ /ₒ s₃) • (ra • r₂ /ₒ (sa * s₁))

Tactic:
rw [oreDiv_smul_oreDiv]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
    oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃) +
      oreNum r₃ (sa * s₁) • ra • r₂ /ₒ (oreDenom r₃ (sa * s₁) * s₃)
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
    oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃) +
      oreNum r₃ (sa * s₁) • ra • r₂ /ₒ (oreDenom r₃ (sa * s₁) * s₃)

Tactic:
rw [oreDiv_smul_oreDiv]

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) =
    oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃) +
      oreNum r₃ (sa * s₁) • ra • r₂ /ₒ (oreDenom r₃ (sa * s₁) * s₃)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ Submonoid.map h.symm.toMonoidHom T = M

Tactic:
← M.map_id,

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ Submonoid.map h.symm.toMonoidHom T = Submonoid.map (MonoidHom.id R) M
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ ↑(adjoin R s) ⊆ ↑(adjoin S s)

Tactic:
rw [← Subalgebra.coe_restrictScalars R (S := S), SetLike.coe_subset_coe]

Goal state after:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ adjoin R s ≤ Subalgebra.restrictScalars R (adjoin S s)
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ CommRing α

Tactic:
apply e.injective.commRing _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: case refine_2.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x y : A ⊗[R] B),
    (∀ (x_1 : A) (y : B), (x_1 ⊗ₜ[R] y * x) • m = x_1 ⊗ₜ[R] y • x • m) →
      (∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = x ⊗ₜ[R] y_1 • y • m) →
        ∀ (x_1 : A) (y_1 : B), (x_1 ⊗ₜ[R] y_1 * (x + y)) • m = x_1 ⊗ₜ[R] y_1 • (x + y) • m

Tactic:
intro z w hz hw a b

Goal state after:
case refine_2.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
hz : ∀ (x : A) (y : B), (x ⊗ₜ[R] y * z) • m = x ⊗ₜ[R] y • z • m
hw : ∀ (x : A) (y : B), (x ⊗ₜ[R] y * w) • m = x ⊗ₜ[R] y • w • m
a : A
b : B
⊢ (a ⊗ₜ[R] b * (z + w)) • m = a ⊗ₜ[R] b • (z + w) • m
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
x : A
y : C
⊢ x ⊗ₜ[R] 1 ⊗ₜ[A] (1 ⊗ₜ[R] y) = 1 ⊗ₜ[A] (x ⊗ₜ[R] y)

Tactic:
trans x • 1 ⊗ₜ[A] (1 ⊗ₜ[R] y)
  · simp [Algebra.smul_def]
  · simp [← tmul_smul, smul_tmul' (M := A)]

Goal state after: