mathlib-initiative/mathlib-tactics huggingface dataset:
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
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • (m₁ + m₂) ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
by rw [smul_add]; exact (A'.1 • M'.1).add_mem h₁ h₂

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
I J : Submodule R A
N : Submodule R M
mn : A
hmn : mn ∈ I ⊔ J
p : M
hp : p ∈ N
⊢ mn • p ∈ I • N ⊔ J • N

Tactic:
obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn

Goal state after:
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
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ (m + n) • p ∈ I • N ⊔ J • N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case mp
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ y ∈ x • p → x⁻¹ * y ∈ p

pp: case mpr
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ x⁻¹ * y ∈ p → y ∈ x • p

Tactic:
· rintro ⟨a, ha : a ∈ p, rfl⟩; simpa [inv_mul_cancel_left₀ hx]

Goal state after:
case mpr
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : DivisionSemiring S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ x⁻¹ * y ∈ p → y ∈ x • p
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
⊢ r • y ∈ s • restrictScalars S N

Tactic:
obtain ⟨c, c_supp, hc⟩ := (mem_set_smul ..).mp <| smul_mem _ r h

Goal state after:
case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
c : R →₀ ↥N
c_supp : ↑c.support ⊆ ⇑(algebraMap S R) '' s
hc : r • y = ↑(c.sum fun r m ↦ r • m)
⊢ r • y ∈ s • restrictScalars S N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type u_1
inst✝⁷ : Semiring R✝
inst✝⁶ : Semiring S
inst✝⁵ : FunLike F R✝ S
f : F
I✝ J : Ideal R✝
K L : Ideal S
G : Type u_2
inst✝⁴ : FunLike G S R✝
inst✝³ : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝² : (i : ι) → Semiring (R i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsPrincipalIdealRing (R i)
I : Ideal ((i : ι) → R i)
⊢ Submodule.IsPrincipal I

Tactic:
by
    rw [← piOrderIso.symm_apply_apply I]
    exact ⟨_, congr(pi $(funext fun i ↦
      (Submodule.IsPrincipal.span_singleton_generator _).symm)).trans pi_span⟩

Goal state after:
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 + z * y) / y = x / y + z

Tactic:
by
  rw [mul_comm z y]
  exact add_mul_div_left _ _ _ h1 h2

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : J ⊔ I = ⊤
⊢ I * K ⊔ J = K ⊔ J

Tactic:
rw [sup_comm, sup_mul_eq_of_coprime_left h, sup_comm]

Goal state after:
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
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : I ⊔ comap f ⊥ = ⊤
⊢ ⊤ ≤ I

Tactic:
exact h ▸ sup_le (le_of_eq rfl) hk

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

Tactic:
· refine (Ideal.mul_le_left.trans (Ideal.mul_le_right.trans
      ((Ideal.pow_le_pow_right ?_).trans le_sup_right)))
    lia

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

Goal state before:
pp: case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ ∀ (a : β) (s : Finset β), a ∉ s → {x ∈ s | f x = 0}.gcd f = 0 → {x ∈ insert a s | f x = 0}.gcd f = 0

Tactic:
· intro a s _ h
        rw [filter_insert]
        split_ifs with h1 <;> simp [h, h1]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
⊢ (s.gcd fun j ↦ f j / s.gcd f) = 1

Tactic:
refine (Finset.gcd_congr rfl fun a ha ↦ ?_).trans hg

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
a : ι
ha : a ∈ s
⊢ f a / s.gcd f = g a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
⊢ a = 0 ∧ b = 0

Tactic:
let ⟨ca, ha⟩ := gcd_dvd_left a b
      let ⟨cb, hb⟩ := gcd_dvd_right a b
      rw [h, zero_mul] at ha hb
      exact ⟨ha, hb⟩

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
b : α
⊢ lcm 0 b = 0

Tactic:
apply lcm_zero_left

Goal state after:
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 _ _) <;>
    rw [dvd_gcd_iff] <;>
    refine ⟨gcd_dvd_left _ _, ?_⟩
  · rcases h with ⟨d, hd⟩
    rcases gcd_dvd_right a b with ⟨e, he⟩
    rcases gcd_dvd_left a b with ⟨f, hf⟩
    use e - f * d
    rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]
  · rcases h with ⟨d, hd⟩
    rcases gcd_dvd_right a c with ⟨e, he⟩
    rcases gcd_dvd_left a c with ⟨f, hf⟩
    use e + f * d
    rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]

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 b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
h0 : lcm c b ≠ 0
⊢ lcm c b * a ∣ c * b

Tactic:
rcases ab with ⟨d, rfl⟩

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 : α
h_1 : ¬a * d = 0
h0 : lcm c (a * d) ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
h0 : lcm c b ≠ 0
⊢ lcm c b * a ∣ c * b

Tactic:
rcases ab with ⟨d, rfl⟩

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 : α
h_1 : ¬a * d = 0
h0 : lcm c (a * d) ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
i : n
⊢ (diagonal d).col i = Pi.single i (d i)

Tactic:
by
  ext
  simp +contextual [diagonal, Pi.single_apply]

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

Tactic:
rw [← not_subsingleton_iff_nontrivial, ← iff_not_comm]
  simp [Module.finrank_eq_zero_iff_of_free]

Goal state after:
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
⊢ Module.rank S M ≤ Module.rank R M

pp: case hc
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
⊢ Module.rank S M < ℵ₀

pp: case hd
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
⊢ Module.rank R M < ℵ₀

Tactic:
· exact rank_top_le_rank_of_isScalarTower R S M

Goal state after:
case hc
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
⊢ Module.rank S M < ℵ₀

case hd
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
⊢ Module.rank R M < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
inj : Injective ⇑f
g : (ℕ →₀ R) →ₗ[R] Fin n → R
hg : Injective ⇑g
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
convert! (Finsupp.basisSingleOne.linearIndependent.map_injOn _ hg.injOn).cardinal_lift_le_rank

Goal state after:
case e'_4
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
inj : Injective ⇑f
g : (ℕ →₀ R) →ₗ[R] Fin n → R
hg : Injective ⇑g
⊢ Module.rank R (Fin n → R) = Cardinal.lift.{0, u} (Module.rank R (Fin n → R))
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ x, (∑ c, (v c • A c) x) * w x = ∑ j, ∑ i, v i * A i j * w j

Tactic:
Pi.smul_apply,

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ x, (∑ x_1, v x_1 • A x_1 x) * w x = ∑ j, ∑ i, v i * A i j * w j
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Nonempty l
inst✝ : Fintype m
A : Matrix m n α
⊢ (Function.Injective fun B ↦ B * A) ↔ Function.Injective fun v ↦ v ᵥ* A

Tactic:
by
  refine ⟨fun ha v w hvw => ?_, fun ha B C hBC => ext_row fun i => ha congr(($hBC).row i)⟩
  inhabit l
  --  `replicateCol` is not available yet
  suffices (of fun i j => v j) = (of fun i j => w j) from
    funext fun j => congrFun₂ this (default : l) j
  exact ha <| ext fun _ _ => congrFun hvw _

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
add_nsmul,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ (n • s + 1 • s).toFinset = s.toFinset
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: case mpr
α : Type u_1
ι : Sort u_3
β : Type u_2
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
t : Set β
x : ↑T
⊢ (∃ i x_1, f i x_1 ∈ t ∧ inclusion ⋯ x_1 = inclusion hT x) → iUnionLift S f hf T hT x ∈ t

Tactic:
rintro ⟨i, ⟨y, hi⟩, h, hxy⟩
    obtain rfl : y = x := congr_arg Subtype.val hxy
    rwa [iUnionLift_of_mem x hi]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (toMultiset f) = f.sum fun x n ↦ Multiset.count a (n • {x})

Tactic:
rw [toMultiset_apply]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (f.sum fun a n ↦ n • {a}) = f.sum fun x n ↦ Multiset.count a (n • {x})
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : R
s : Set A
⊢ adjoin R (insert ((algebraMap R A) x) s) = adjoin R s

Tactic:
rw [Set.insert_eq, adjoin_union]

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : R
s : Set A
⊢ R[(algebraMap R A) x] ⊔ adjoin R s = adjoin R s
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarAddMonoid R
⊢ Commute (star 0) 0

Tactic:
by simp only [Commute.refl, star_zero]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = diagonal (Sum.elim d₁ d₂)

Tactic:
by
  ext i j
  rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [diagonal]

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

Goal state before:
pp: α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
⊢ of (vecCons v A) *ᵥ w = vecCons (v ⬝ᵥ w) (of A *ᵥ w)

Tactic:
by
  ext i
  refine Fin.cases ?_ ?_ i <;> simp [mulVec]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e f : M ≃ₗ[R] M
⊢ LinearEquiv.baseChange R A M M (e * f) = LinearEquiv.baseChange R A M M e * LinearEquiv.baseChange R A M M f

Tactic:
by
  simp [LinearEquiv.mul_eq_trans, LinearEquiv.baseChange_trans]

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

Goal state before:
pp: case c.c.c.e_a.e_a
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₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ ra • r₂ /ₒ (sa * s₁) = r₂ /ₒ s₂

Tactic:
rw [OreLocalization.expand r₂ s₂ ra (ha.symm ▸ (sa * s₁).2)]

Goal state after:
case c.c.c.e_a.e_a
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₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ ra • r₂ /ₒ (sa * s₁) = ra • r₂ /ₒ ⟨ra * ↑s₂, ⋯⟩
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:
by
  rw [← commClosure_eq_closure]; rfl

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

Goal state before:
pp: R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
⊢ basisOfPid b ⊥ = ⟨0, Basis.empty ↥⊥⟩

Tactic:
obtain ⟨n, b'⟩ := Submodule.basisOfPid b ⊥

Goal state after:
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
⊢ ⟨n, b'⟩ = ⟨0, Basis.empty ↥⊥⟩
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r : R i
s : ↥S
⊢ ∃ a, (mapPiEvalRingHom S) a = mk' (Localization S) r s

Tactic:
exact ⟨mk' (M := T) _ (update 0 i r) ⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩,
      by simp [map_mk']⟩

Goal state after:
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)
⊢ ∀ (x y : S),
    (↑((toLocalizationMap M S).lift₀ g.toMonoidWithZeroHom hg)).toFun (x + y) =
      (↑((toLocalizationMap M S).lift₀ g.toMonoidWithZeroHom hg)).toFun x +
        (↑((toLocalizationMap M S).lift₀ g.toMonoidWithZeroHom hg)).toFun y

Tactic:
intro x y
      dsimp
      rw [(toLocalizationMap M S).lift₀_def, (toLocalizationMap M S).lift_spec,
        mul_add, mul_comm, eq_comm, lift_spec_mul_add, add_comm, mul_comm, mul_assoc, mul_comm,
        mul_assoc, lift_spec_mul_add]
      simp_rw [← mul_assoc]
      change g _ * g _ * g _ + g _ * g _ * g _ = g _ * g _ * g _
      simp_rw [← map_mul g, ← map_add g]
      apply eq_of_eq (S := S) hg
      simp only [sec_spec', toLocalizationMap_sec, map_add, map_mul]
      ring

Goal state after:
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
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommSemiring T
f : S →+* T
⊢ Injective ⇑f ↔ ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ f ((algebraMap R S) x) = f ((algebraMap R S) y)

Tactic:
rw [← IsLocalization.lift_of_comp (M := M) f, IsLocalization.lift_injective_iff]
  simp

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

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✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ IsLocalization M P

Tactic:
constructor; constructor
  · intro y
    convert! (IsLocalization.map_units S y).map h.toAlgHom.toRingHom.toMonoidHom
    exact (h.commutes y).symm
  · intro y
    obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M (h.symm y)
    apply_fun (show S → P from h) at e
    simp only [map_mul, h.apply_symm_apply, h.commutes] at e
    exact ⟨⟨x, s⟩, e⟩
  · intro x y
    rw [← h.symm.toEquiv.injective.eq_iff, ← IsLocalization.eq_iff_exists M S, ← h.symm.commutes, ←
      h.symm.commutes]
    exact id

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

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
surj : ∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y
inj : Function.Injective ⇑(algebraMap R K)
this✝ : NoZeroDivisors R
this : Nontrivial R
z : K
x : R
eq : z = (algebraMap R K) x / (algebraMap R K) 0
⊢ ∃ x, z * (algebraMap R K) ↑x.2 = (algebraMap R K) x.1

Tactic:
obtain rfl : z = 0 := by simpa using eq

Goal state after:
case inl
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
surj : ∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y
inj : Function.Injective ⇑(algebraMap R K)
this✝ : NoZeroDivisors R
this : Nontrivial R
x : R
eq : 0 = (algebraMap R K) x / (algebraMap R K) 0
⊢ ∃ x, 0 * (algebraMap R K) ↑x.2 = (algebraMap R K) x.1
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective ⇑(algebraMap R S)

Tactic:
by
  refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective R K)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : N ⊗[R] M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, x = (rTensor M J.subtype) y

Tactic:
by
  induction x with
  | zero => exact ⟨⊥, fg_bot, 0, rfl⟩
  | tmul i m => exact ⟨R ∙ i, fg_span_singleton i, ⟨i, mem_span_singleton_self _⟩ ⊗ₜ[R] m, rfl⟩
  | add x₁ x₂ ihx₁ ihx₂ =>
    obtain ⟨J₁, fg₁, y₁, rfl⟩ := ihx₁
    obtain ⟨J₂, fg₂, y₂, rfl⟩ := ihx₂
    refine ⟨J₁ ⊔ J₂, fg₁.sup fg₂,
      rTensor M (J₁.inclusion le_sup_left) y₁ + rTensor M (J₂.inclusion le_sup_right) y₂, ?_⟩
    rw [map_add, ← rTensor_comp_apply, ← rTensor_comp_apply]
    rfl

Goal state after: