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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length < ↑↑0 ↔ ∀ (l : LTSeries α), l.length < 0

Tactic:
rw [ENat.natCast_zero, ← bot_eq_zero, WithBot.lt_coe_bot]
    simp

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x ↦
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
⊢ ↑p.length ≤ height x + 1

Tactic:
have hlast' : p'.last = x := by
      simp only [p', RelSeries.last, WithBot.unbot_eq_iff, ← hlast, Fin.last]
      congr
      lia

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x ↦
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p.length ≤ height x + 1
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
n : ℕ
x : M ⊗[R] N
⊢ -↑n.succ • x = -((↑n + 1) • x)

Tactic:
← zero_add (_ • x),

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
S : Type u_6
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
n : ℕ
x : M ⊗[R] N
⊢ 0 + -↑n.succ • x = -((↑n + 1) • x)
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mpr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
g : ι → α
hg : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1
⊢ ∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = g i * ∏ i ∈ is, g i

Tactic:
exact ⟨g i, hg (is.mem_insert_self _), is.prod g,
        ⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t t₁ : M ⊗[R] N
⊢ ∀ (y : M ⊗[R] N),
    t₁ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} →
      y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → t₁ + y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
t₂

Goal state after:
case refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t t₁ t₂ : M ⊗[R] N
⊢ t₁ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} →
    t₂ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → t₁ + t₂ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.map (map f g) (Submodule.map₂ (mk R M N) ⊤ ⊤) = Submodule.map₂ ((mk R P Q).compl₁₂ f g) ⊤ ⊤

Tactic:
Submodule.map_map₂

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.map₂ ((mk R M N).compr₂ (map f g)) ⊤ ⊤ = Submodule.map₂ ((mk R P Q).compl₁₂ f g) ⊤ ⊤
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_7
P : Type u_9
Q : Type u_10
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R M
inst✝¹ : Module R P
inst✝ : Module R Q
f : P →ₗ[R] Q →ₗ[R] M
p : Submodule R P
q : Submodule R Q
⊢ Submodule.map₂ f p q = Submodule.map (lift f) (Submodule.map₂ (mk R P Q) p q)

Tactic:
Submodule.map_map₂

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_7
P : Type u_9
Q : Type u_10
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R M
inst✝¹ : Module R P
inst✝ : Module R Q
f : P →ₗ[R] Q →ₗ[R] M
p : Submodule R P
q : Submodule R Q
⊢ Submodule.map₂ f p q = Submodule.map₂ ((mk R P Q).compr₂ (lift f)) p q
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a b : α
hb : 1 ≤ b
⊢ a * b ≤ b → a∗ ≤ b

Tactic:
simpa using kstar_mul_le hb

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
⊢ 1 + a * (1 + a * a∗) ≤ 1 + a * a∗

Tactic:
apply add_le_add_right (mul_right_mono h)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z

Tactic:
← mul_one z,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * 1
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
rw [mul_comm] at h
  exact h.of_add_mul_left_right

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

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

Tactic:
by
  rw [add_comm]
  exact h.add_mul_left_left z

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
x : I
hx : x ∈ t
⊢ a ∈ insert a t \ {x}

Tactic:
mem_sdiff,

Goal state after:
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
x : I
hx : x ∈ t
⊢ a ∈ insert a t ∧ a ∉ {x}
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy : (fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)) y = S
⊢ S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)

Tactic:
obtain ⟨y', hy', fy_eq⟩ := mem_map.mp y.2
        use ⟨y', hy'⟩
        refine Eq.trans ?_ hy
        rw [f.toLinearMap_apply] at fy_eq
        ext
        simp [fy_eq]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
n : ℕ
⊢ map (↑(opLinearEquiv R)) (M ^ n) = map (↑(opLinearEquiv R)) M ^ n

Tactic:
by
  rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ MonoidHom.mker (spanSingleton R) = Submonoid.map (algebraMap R A) (IsUnit.submonoid R)

Tactic:
ext; simp_rw [Submonoid.mem_map, IsUnit.mem_submonoid_iff, IsUnit, existsAndEq, true_and, eq_comm]
  exact span_singleton_eq_one_iff

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

Goal state before:
pp: case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ I ≠ ⊤

pp: case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
· contrapose h
    rw [h, prod_top_top, isPrime_iff]
    simp

Goal state after:
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : (I.prod ⊤).IsPrime
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
N : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
S : Submodule R N
x✝ : IsNoetherian R ↥S ∧ IsNoetherian R (N ⧸ S)
left✝ : IsNoetherian R ↥S
right✝ : IsNoetherian R (N ⧸ S)
⊢ S.subtype.range = S.mkQ.ker

Tactic:
Submodule.ker_mkQ,

Goal state after:
R : Type u_1
N : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
S : Submodule R N
x✝ : IsNoetherian R ↥S ∧ IsNoetherian R (N ⧸ S)
left✝ : IsNoetherian R ↥S
right✝ : IsNoetherian R (N ⧸ S)
⊢ S.subtype.range = S
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
⊢ (∃ x ∈ pi I, (Pi.evalRingHom R i) x = r) ↔ r ∈ I i

Tactic:
classical refine ⟨?_, fun hr ↦ ⟨_, single_mem_pi hr, by simp⟩⟩

Goal state after:
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
⊢ (∃ x ∈ pi I, (Pi.evalRingHom R i) x = r) → r ∈ I i
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* R
g : T →+* S
⊢ Ideal.comap g (Ideal.comap f ⊥) = ker (f.comp g)

Tactic:
Ideal.comap_comap,

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* R
g : T →+* S
⊢ Ideal.comap (f.comp g) ⊥ = ker (f.comp g)
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
apply eq_div_of_mul_eq_right hz

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
simp only [h, dedup_cons_of_mem, IH, gcd_cons]

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ s.gcd = GCDMonoid.gcd a s.gcd
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
⊢ map f (sInf {J | I ≤ J ∧ J.IsPrime}) = (map f I).radical

Tactic:
radical_eq_sInf

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
⊢ map f (sInf {J | I ≤ J ∧ J.IsPrime}) = sInf {J | map f I ≤ J ∧ J.IsPrime}
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: i j : ℤ
⊢ 0 ≤ GCDMonoid.gcd i j

Tactic:
by simp [← coe_gcd]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
s : Multiset (Ideal R)
h : ∀ p ∈ s, I ⊔ p = ⊤
⊢ I ⊔ 1 = ⊤

Tactic:
simp only [one_eq_top, le_top, sup_of_le_right]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
⊢ ker (Pi.evalRingHom R i) = Ideal.span {1 - Pi.single i 1}

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (by simp [Ideal.span_le])

Goal state after:
ι : Type u_1
inst✝¹ : DecidableEq ι
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
⊢ x ∈ Ideal.span {1 - Pi.single i 1}
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
⊢ Associated a b → normalize a = normalize b

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
u : αˣ
⊢ normalize a = normalize (a * ↑u)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
⊢ I ⊔ J = ⊤

Tactic:
by_contra hIJ

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
hIJ : ¬I ⊔ J = ⊤
⊢ False
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case insert
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : (↑s).Pairwise (IsCoprime on J) → ∏ i ∈ s, J i = ⨅ i ∈ s, J i
hp : (↑(insert a s)).Pairwise (IsCoprime on J)
⊢ ∏ i ∈ insert a s, J i = ⨅ i ∈ insert a s, J i

Tactic:
simp_all only [Finset.iInf_insert, Finset.coe_insert, Set.pairwise_insert, SetLike.mem_coe,
      ne_eq, not_false_eq_true, Finset.prod_insert, forall_const]
    obtain ⟨hp1, hp2⟩ := hp
    rw [Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ↑(Classical.choose ⋯) = ↑(Classical.choose ⋯) * ↑(Classical.choose ⋯)

Tactic:
suffices a * b * ↑(Classical.choose (associated_map_mk hinv (a * b))) =
        a * ↑(Classical.choose (associated_map_mk hinv a)) *
        (b * ↑(Classical.choose (associated_map_mk hinv b))) by
      apply mul_left_cancel₀ (mul_ne_zero ha hb) _
      simpa only [mul_assoc, mul_comm, mul_left_comm] using this

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * ↑(Classical.choose ⋯) = a * ↑(Classical.choose ⋯) * (b * ↑(Classical.choose ⋯))
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * ↑u + s.gcd f * y * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a

Tactic:
refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩

Goal state after:
case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * ↑u + s.gcd f * y * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ (insert a s).gcd f = ∑ a_1 ∈ insert a s, f a_1 * update (fun x ↦ g x * (y * ↑u)) a (x * ↑u) a_1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ↑(f b) ∪ ⋃ x ∈ ↑t, ↑(f x)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : f a ≤ f i
⊢ ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)

Tactic:
Set.union_eq_self_of_subset_left Ha

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ x ∈ ↑t, ↑(f x)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : f a ≤ f i
⊢ ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
intro i hiu

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a (insert b u)), ↑(f i)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
⊢ (f i).IsPrime
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
Finset.exists_mem_insert,

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ I ≤ f a ∨ ∃ x ∈ insert b u, I ≤ f x
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
hbs : b ∉ s
hsne : s.Nonempty
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
obtain ⟨i, his⟩ := hsne

Goal state after:
case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
hbs : b ∉ s
i : ι
his : i ∈ s
⊢ ∃ i ∈ s, I ≤ f i
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
⊢ (∑ i_1, if i = i' ∧ j = i_1 then c * x i_1 else 0) = Function.update 0 i (c * x j) i'

Tactic:
rcases eq_or_ne i i' with rfl | h

Goal state after:
case inl
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
⊢ (∑ i_1, if i = i ∧ j = i_1 then c * x i_1 else 0) = Function.update 0 i (c * x j) i

case inr
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
h : i ≠ i'
⊢ (∑ i_1, if i = i' ∧ j = i_1 then c * x i_1 else 0) = Function.update 0 i (c * x j) i'
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ ↑M ⊆ ⋃ I ∈ S, ↑I ↔ M ∈ S

Tactic:
by
  refine (subset_union_prime_finite hs a b hp).trans ⟨fun ⟨I, mem, le⟩ ↦ ?_, (⟨M, ·, le_rfl⟩)⟩
  rwa [‹M.IsMaximal›.eq_of_le _ le]
  simp_rw [← or_iff_not_imp_left] at hp
  obtain rfl | rfl | hp := hp I mem
  exacts [ha, hb, hp.ne_top]

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

Goal state before:
pp: case inr
R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : OrzechProperty R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : M →ₗ[R] M'
hf : Surjective ⇑f
h : finrank R M ≤ finrank R M'
h✝ : Nontrivial R
w✝ : M →ₗ[R] M'
hi : Injective ⇑w✝
⊢ Bijective ⇑f

Tactic:
exact OrzechProperty.bijective_of_surjective_of_injective _ _ hi hf

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

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ⨁ (i : ι), β i
i : ι
⊢ (∑ i, (of β i) (x i)) i = x i

Tactic:
simp [of_apply]

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 : Set (Subalgebra R A)
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
x : R
y : Subalgebra R A
hy : y ∈ S
⊢ ∃ a ∈ S, (algebraMap R A) x ∈ a

Tactic:
exact ⟨y, hy, algebraMap_mem y x⟩

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

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ Subalgebra.toSubmodule (adjoin R (s ∪ t)) = Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t)

Tactic:
by
  rw [adjoin_eq_span, adjoin_eq_span, adjoin_eq_span, span_mul_span]
  congr 1 with z; simp [Submonoid.closure_union, Submonoid.mem_sup, Set.mem_mul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ b * c * r • a = b * (c * r • a)

Tactic:
by
    rw [mul_smul_comm, mul_smul_comm, mul_smul_comm, ha.right_assoc]

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

Goal state before:
pp: case i
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
⊢ M ⊗[R₀] (N →₀ R₀) →ₗ[R] (M →₀ R) ⊗[R₀] (N →₀ R₀)

Tactic:
exact (AlgebraTensorModule.map sM (LinearMap.id (R := R₀) (M := N →₀ R₀)))

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : IsUnit a
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ

pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ

Tactic:
· obtain ⟨u, rfl⟩ := ha
    rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a u : R
hu : IsUnit u
⊢ IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a

Tactic:
by
  simpa using hu.star.isSelfAdjoint_conjugate_iff

Goal state after: