mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
have : Associated (a * b) 0 := (gcd_mul_lcm a b).symm.trans <| by rw [h, mul_zero]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
this : Associated (a * b) 0
⊢ a = 0 ∨ b = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : I ^ n ≤ P ↔ ∃ I_1, (¬False ∧ I_1 = I) ∧ I_1 ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P

Tactic:
not_false_eq_true,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : I ^ n ≤ P ↔ ∃ I_1, (True ∧ I_1 = I) ∧ I_1 ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
r : R
⊢ Associated (generator (Ideal.span {r})) r

Tactic:
← Ideal.span_singleton_eq_span_singleton

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
r : R
⊢ Ideal.span {generator (Ideal.span {r})} = Ideal.span {r}
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi fun x ↦ I
a b : ι → R
hab : (Submodule.quotientRel (Ideal.pi fun x ↦ I)) a b
h : ι'
⊢ (e a - e b) h ∈ (fun x ↦ I) h

Tactic:
rw [Submodule.quotientRel_def] at hab
      rw [← map_sub]
      exact Ideal.map_pi _ _ hab e h

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

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a✝ : Associates α
a : α
b✝ : Associates α
b : α
⊢ Associated
    (Quotient.map₂ gcd ⋯ (Quot.mk (⇑(Associated.setoid α)) a) (Quot.mk (⇑(Associated.setoid α)) b) *
      Quotient.map₂ lcm ⋯ (Quot.mk (⇑(Associated.setoid α)) a) (Quot.mk (⇑(Associated.setoid α)) b))
    (Quot.mk (⇑(Associated.setoid α)) a * Quot.mk (⇑(Associated.setoid α)) b)

Tactic:
rw [associated_iff_eq]

Goal state after:
case mk.mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a✝ : Associates α
a : α
b✝ : Associates α
b : α
⊢ Quotient.map₂ gcd ⋯ (Quot.mk (⇑(Associated.setoid α)) a) (Quot.mk (⇑(Associated.setoid α)) b) *
      Quotient.map₂ lcm ⋯ (Quot.mk (⇑(Associated.setoid α)) a) (Quot.mk (⇑(Associated.setoid α)) b) =
    Quot.mk (⇑(Associated.setoid α)) a * Quot.mk (⇑(Associated.setoid α)) b
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Unique m
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
⊢ diagonal d = of fun x x_1 ↦ d default

Tactic:
ext i j
  rw [Subsingleton.elim i default, Subsingleton.elim j default, diagonal_apply_eq _ _, of_apply]

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

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

Tactic:
exact this.symm ▸ i

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✝ : Module.Finite R M
⊢ ↑(finrank R M) = Module.rank R M

Tactic:
by
  rw [Module.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]

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

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
x : M
inst✝ : Module.Finite K ↥(span K s)
⊢ x ∈ span K s ↔ ∃ c, c.support.card ≤ finrank K ↥(span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x

Tactic:
constructor
  · intro h
    rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, ht_sub, ht_card, ht_span, ht_indep⟩
    rcases mem_span_set.mp (ht_span ▸ h) with ⟨c, hct, hx⟩
    refine ⟨c, ?_, hct.trans ht_sub, hx⟩
    exact ht_card ▸ Finset.card_mono hct
  · rintro ⟨c, -, hcs, hx⟩
    exact mem_span_set.mpr ⟨c, hcs, hx⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ z * i * x + i * i ^ n + y * x = 1

Tactic:
rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa

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:
by
    ext
    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:
by
  dsimp [liftLinear, -LinearMap.lsum_apply, LinearEquiv.congrLeft, LinearEquiv.piCongrRight]
  simp_rw [of_symm_single, LinearMap.lsum_piSingle]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
⊢ Function.Injective mulVec

Tactic:
intro A B h

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
h : A.mulVec = B.mulVec
⊢ A = B
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
⊢ Function.Injective fun x v ↦ v ᵥ* x

Tactic:
intro A B h

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
h : (fun x v ↦ v ᵥ* x) A = (fun x v ↦ v ᵥ* x) B
⊢ A = B
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Zero β
⊢ #(α →₀ β) = lift.{u, v} #β ^ Fintype.card α

Tactic:
simpa using (@Finsupp.equivFunOnFinite α β _ _).cardinal_eq

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α × β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
⊢ Nonempty (R ≃ₗ[R] M) ↔ Module.rank R M = 1

Tactic:
by
  simp [nonempty_linearEquiv_iff_lift_rank_eq, eq_comm]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
this✝² : Nontrivial R
this✝¹ : Module.Finite R M
this✝ : Finite ι
this : Fintype ι
d1 : Fintype.card ι = 1
⊢ Nonempty (Unique ι)

Tactic:
Fintype.card_eq_one_iff_nonempty_unique

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
this✝² : Nontrivial R
this✝¹ : Module.Finite R M
this✝ : Finite ι
this : Fintype ι
d1 : Nonempty (Unique ι)
⊢ Nonempty (Unique ι)
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
M : Type u_1
S : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike S M
inst✝² : AddSubmonoidClass S M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ (m ∈ support fun i ↦ ↑(x i)) → m ∈ ↑(DFinsupp.support x)

Tactic:
simp only [Function.mem_support, Finset.mem_coe, DFinsupp.mem_support_toFun, not_imp_not,
    ZeroMemClass.coe_eq_zero, imp_self]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ (S ⊔ T).toSubsemiring = Subsemiring.closure (↑S.toSubsemiring ∪ ↑T.toSubsemiring)

Tactic:
sup_def,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ (adjoin R (↑S ∪ ↑T)).toSubsemiring = Subsemiring.closure (↑S.toSubsemiring ∪ ↑T.toSubsemiring)
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
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s
⊢ 0 ∈ s

Tactic:
simpa using h.2.2 0

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ iSup A = ⊤

Tactic:
by
  rw [Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top]
  exact Function.Bijective.surjective h

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

Goal state before:
pp: case a.mem
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x : A
hx : x ∈ s
⊢ x ∈ span R ↑(Subsemigroup.closure s)

Tactic:
| mem x hx =>

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

Goal state before:
pp: case a.cons.cons.inl
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hd : R
HL : (algebraMap R A) hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (hd * z) • r = (algebraMap R A) hd * z • r

Tactic:
rw [Algebra.smul_def, Algebra.smul_def, (algebraMap _ _).map_mul, _root_.mul_assoc]

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

Goal state before:
pp: case mem
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
x : A
hx : x ∈ s
⊢ Commute a x

Tactic:
| mem x hx =>

Goal state after:
Module: Mathlib.Algebra.Field.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ unop ↑q = unop (↑q.num / ↑q.den)

Tactic:
unop_ratCast,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ ↑q = unop (↑q.num / ↑q.den)
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝² : InvolutiveStar R
inst✝¹ : SetLike S R
inst✝ : StarMemClass S R
s : S
r : R
hr : star r ∈ s
⊢ r ∈ s

Tactic:
← star_star r

Goal state after:
S : Type u_1
R : Type u_2
inst✝² : InvolutiveStar R
inst✝¹ : SetLike S R
inst✝ : StarMemClass S R
s : S
r : R
hr : star r ∈ s
⊢ star (star r) ∈ s
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: A : Type u_2
a : A
inst✝¹ : Semiring A
inst✝ : StarRing A
ha : IsSelfAdjoint a
⊢ IsSelfAdjoint a⁻¹ʳ

Tactic:
by
  rw [isSelfAdjoint_iff, ← Ring.inverse_star, ha.star_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: ι : 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'
i : ι
⊢ b.repr ((b.prod b') (Sum.inl i)).1 = b.repr (b i)

Tactic:
ext j
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Finsupp.fst_sumFinsuppLEquivProdFinsupp]
    apply Finsupp.single_apply_left Sum.inl_injective

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
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✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map (b • f) g = b • map f g

Tactic:
by
  ext
  simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul,
    smul_apply, smul_tmul']

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
⊢ False

Tactic:
simp only [hr, pow_one, mul_assoc, eq_comm (a := r), mul_eq_left, LeftCancelMonoid.mul_eq_one,
      Finset.prod_eq_one_iff] at hr'

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
⊢ False
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : S.LocalizationMap N
⊢ f 0 = 0

Tactic:
have ⟨ms, eq⟩ := f.surj 0
    rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]

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

Goal state before:
pp: R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R⁰ R
h : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
by
  induction x with | _ r s
  rw [OreLocalization.inv_def, OreLocalization.one_def]
  have hr : r ≠ 0 := by
    rintro rfl
    simp at h
  simp only [hr]
  with_unfolding_all apply OreLocalization.mul_inv ⟨r, _⟩

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

Goal state before:
pp: case pos
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
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : N = ⊥
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

pp: case neg
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
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : ¬N = ⊥
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Tactic:
· subst N_bot
    exact ⟨0, ⟨Basis.empty _⟩⟩

Goal state after:
case neg
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
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : ¬N = ⊥
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M N : 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)
H : M ≤ IsUnit.submonoid R
⊢ R ≃ₐ[R] S

Tactic:
by
  refine AlgEquiv.ofBijective (Algebra.ofId R S) ⟨?_, ?_⟩
  · intro x y hxy
    obtain ⟨c, eq⟩ := (IsLocalization.eq_iff_exists M S).mp hxy
    obtain ⟨u, hu⟩ := H c.prop
    rwa [← hu, Units.mul_right_inj] at eq
  · intro y
    obtain ⟨⟨x, s⟩, eq⟩ := IsLocalization.surj M y
    obtain ⟨u, hu⟩ := H s.prop
    use x * u.inv
    dsimp [Algebra.ofId, RingHom.toFun_eq_coe, AlgHom.coe_mks]
    rw [map_mul, ← eq, ← hu, mul_assoc, ← map_mul]
    simp

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
⊢ (adjoin R s).prod (adjoin R t) ≤ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
· rintro ⟨a, b⟩ ⟨ha, hb⟩
    let P := adjoin R (LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1}))
    have Ha : (a, (0 : B)) ∈ adjoin R (LinearMap.inl R A B '' (s ∪ {1})) :=
      mem_adjoin_of_map_mul R LinearMap.inl_map_mul ha
    have Hb : ((0 : A), b) ∈ adjoin R (LinearMap.inr R A B '' (t ∪ {1})) :=
      mem_adjoin_of_map_mul R LinearMap.inr_map_mul hb
    replace Ha : (a, (0 : B)) ∈ P := adjoin_mono Set.subset_union_left Ha
    replace Hb : ((0 : A), b) ∈ P := adjoin_mono Set.subset_union_right Hb
    simpa [P] using Subalgebra.add_mem _ Ha Hb

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap S₂ T) ((algebraMap R S₂) n) =
    (algebraMap S₁ T) ((algebraMap R S₁) z) * (algebraMap S₁ T) ↑hunit.unit⁻¹

Tactic:
conv_rhs => rw [← IsScalarTower.algebraMap_apply]

Goal state after:
case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap S₂ T) ((algebraMap R S₂) n) = (algebraMap R T) z * (algebraMap S₁ T) ↑hunit.unit⁻¹
Module: Mathlib.RingTheory.Localization.Defs

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

Tactic:
rw [add_comm (b * c) (d * a), mul_comm b d]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ mk a b + mk c d = mk (↑d * a + ↑b * c) (d * b)
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal

Tactic:
let s := { m : ℕ | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤ }

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
⊢ ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ IsIdempotentElem (q - p) ∧ IsSelfAdjoint (q - p) ↔ p * q = p

Tactic:
hp.isIdempotentElem.sub_iff hq.isIdempotentElem

Goal state after:
R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ (p * q = p ∧ q * p = p) ∧ IsSelfAdjoint (q - p) ↔ p * q = p
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
⊢ ∀ (a_1 : R), Commute (star a) a_1

Tactic:
by simpa only [star_mul, star_star] using! fun g =>
    congr_arg star ((mem_center_iff.1 ha).comm <| star g).symm

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
s : R
r : Rˣ
⊢ r • s ∈ σ (r • a) ↔ s ∈ σ a

Tactic:
simp only [mem_iff, Algebra.algebraMap_eq_smul_one, smul_assoc, ← smul_sub, isUnit_smul_iff]

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

Goal state before:
pp: case mpr
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ x ∈ r • σ a → r⁻¹ • x ∈ σ a

Tactic:
· rintro ⟨w, _, (x'_eq : r • w = x)⟩
    simpa [← x'_eq]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ {r} + -σ a = σ (↑ₐ r - a)

Tactic:
neg_eq,

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ {r} + σ (-a) = σ (↑ₐ r - a)