mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁵⁰ : CommSemiring R
inst✝⁴⁹ : CommSemiring R₂
inst✝⁴⁸ : CommSemiring R₃
inst✝⁴⁷ : Monoid R'
inst✝⁴⁶ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A✝ : Type u_6
M✝ : Type u_7
N✝ : Type u_8
P : Type u_9
Q : Type u_10
S✝ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁵ : AddCommMonoid M✝
inst✝⁴⁴ : AddCommMonoid N✝
inst✝⁴³ : AddCommMonoid P
inst✝⁴² : AddCommMonoid Q
inst✝⁴¹ : AddCommMonoid S✝
inst✝⁴⁰ : AddCommMonoid P'
inst✝³⁹ : AddCommMonoid Q'
inst✝³⁸ : AddCommMonoid M₂
inst✝³⁷ : AddCommMonoid N₂
inst✝³⁶ : AddCommMonoid P₂
inst✝³⁵ : AddCommMonoid Q₂
inst✝³⁴ : AddCommMonoid M₃
inst✝³³ : AddCommMonoid N₃
inst✝³² : AddCommMonoid P₃
inst✝³¹ : AddCommMonoid Q₃
inst✝³⁰ : DistribMulAction R' M✝
inst✝²⁹ : Module R'' M✝
inst✝²⁸ : Module R M✝
inst✝²⁷ : Module R N✝
inst✝²⁶ : Module R S✝
inst✝²⁵ : Module R P'
inst✝²⁴ : Module R Q'
inst✝²³ : Module R₂ M₂
inst✝²² : Module R₂ N₂
inst✝²¹ : Module R₂ P₂
inst✝²⁰ : Module R₂ Q₂
inst✝¹⁹ : Module R₃ M₃
inst✝¹⁸ : Module R₃ N₃
inst✝¹⁷ : Module R₃ P₃
inst✝¹⁶ : Module R₃ Q₃
inst✝¹⁵ : Module R P
inst✝¹⁴ : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : CommSemiring A
inst✝⁸ : Module A M
inst✝⁷ : Module A N
inst✝⁶ : SMulCommClass R A M
inst✝⁵ : CommSemiring S
inst✝⁴ : Module S M
inst✝³ : SMulCommClass R S M
inst✝² : SMulCommClass A S M
inst✝¹ : CompatibleSMul R A M N
inst✝ : CompatibleSMul A R M N
x x✝¹ x✝ : M ⊗[A] N
h : (mapOfCompatibleSMul A R S M N) ((mapOfCompatibleSMul R A S M N).toFun x✝¹) = x✝¹
h' : (mapOfCompatibleSMul A R S M N) ((mapOfCompatibleSMul R A S M N).toFun x✝) = x✝
⊢ (mapOfCompatibleSMul A R S M N) ((mapOfCompatibleSMul R A S M N).toFun (x✝¹ + x✝)) = x✝¹ + x✝

Tactic:
by simpa using congr($h + $h')

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁵⁰ : CommSemiring R
inst✝⁴⁹ : CommSemiring R₂
inst✝⁴⁸ : CommSemiring R₃
inst✝⁴⁷ : Monoid R'
inst✝⁴⁶ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A✝ : Type u_6
M✝ : Type u_7
N✝ : Type u_8
P : Type u_9
Q : Type u_10
S✝ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁵ : AddCommMonoid M✝
inst✝⁴⁴ : AddCommMonoid N✝
inst✝⁴³ : AddCommMonoid P
inst✝⁴² : AddCommMonoid Q
inst✝⁴¹ : AddCommMonoid S✝
inst✝⁴⁰ : AddCommMonoid P'
inst✝³⁹ : AddCommMonoid Q'
inst✝³⁸ : AddCommMonoid M₂
inst✝³⁷ : AddCommMonoid N₂
inst✝³⁶ : AddCommMonoid P₂
inst✝³⁵ : AddCommMonoid Q₂
inst✝³⁴ : AddCommMonoid M₃
inst✝³³ : AddCommMonoid N₃
inst✝³² : AddCommMonoid P₃
inst✝³¹ : AddCommMonoid Q₃
inst✝³⁰ : DistribMulAction R' M✝
inst✝²⁹ : Module R'' M✝
inst✝²⁸ : Module R M✝
inst✝²⁷ : Module R N✝
inst✝²⁶ : Module R S✝
inst✝²⁵ : Module R P'
inst✝²⁴ : Module R Q'
inst✝²³ : Module R₂ M₂
inst✝²² : Module R₂ N₂
inst✝²¹ : Module R₂ P₂
inst✝²⁰ : Module R₂ Q₂
inst✝¹⁹ : Module R₃ M₃
inst✝¹⁸ : Module R₃ N₃
inst✝¹⁷ : Module R₃ P₃
inst✝¹⁶ : Module R₃ Q₃
inst✝¹⁵ : Module R P
inst✝¹⁴ : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : CommSemiring A
inst✝⁸ : Module A M
inst✝⁷ : Module A N
inst✝⁶ : SMulCommClass R A M
inst✝⁵ : CommSemiring S
inst✝⁴ : Module S M
inst✝³ : SMulCommClass R S M
inst✝² : SMulCommClass A S M
inst✝¹ : CompatibleSMul R A M N
inst✝ : CompatibleSMul A R M N
x x✝¹ x✝ : M ⊗[R] N
h : (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) x✝¹) = x✝¹
h' : (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) x✝) = x✝
⊢ (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) (x✝¹ + x✝)) = x✝¹ + x✝

Tactic:
by simpa using congr($h + $h')

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
t : Multiset ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
⊢ (Multiset.map f₁ t).prod ⊆ (Multiset.map f₂ t).prod

Tactic:
by
  induction t using Quotient.inductionOn
  simp_rw [Multiset.quot_mk_to_coe, Multiset.map_coe, Multiset.prod_coe]
  exact list_prod_subset_list_prod _ _ _ hf

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : AddMonoidWithOne R
⊢ 1 = closure {1}

Tactic:
rw [closure_singleton_eq, one_eq_mrange]

Goal state after:
R : Type u_2
inst✝ : AddMonoidWithOne R
⊢ AddMonoidHom.mrange (Nat.castAddMonoidHom R) = AddMonoidHom.mrange ((multiplesHom R) 1)
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
s : Set R
n : ℕ
⊢ closure (s ^ n) * closure s = closure (s ^ n * s)

Tactic:
closure_mul_closure

Goal state after:
R : Type u_2
inst✝ : Semiring R
s : Set R
n : ℕ
⊢ closure (s ^ n * s) = closure (s ^ n * s)
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
by
  rw [isCoprime_comm] at H1 H2 ⊢
  exact H1.mul_left H2

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

Goal state before:
pp: case h₂
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 * (b * y)

Tactic:
· rw [mul_comm b, ← mul_assoc]
    exact (mul_dvd_mul_right H1 _).mul_right _

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
⊢ a ^ 2 + b ^ 2 ≠ 0

Tactic:
intro h'

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ False
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
inst✝ : IsScalarTower R A A
N P : Submodule R A
h : N * P = 1
⊢ ⊤ ≤ N * ⊤

Tactic:
conv_lhs => rw [← Submodule.one_mul ⊤, ← h, mul_assoc]

Goal state after:
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
N P : Submodule R A
h : N * P = 1
⊢ N * (P * ⊤) ≤ N * ⊤
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 N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ (range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) =
    range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)

Tactic:
ext S

Goal state after:
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'
⊢ (S ∈ range fun i ↦ map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)) ↔
    S ∈ range fun s ↦ map ((LinearMap.mul R A') ↑s) (map f.toLinearMap N)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝⁶ : CommSemiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
S✝ T✝ : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst✝³ : Monoid α
inst✝² : DistribMulAction α A
inst✝¹ : SMulCommClass α R A
inst✝ : IsScalarTower α A A
a : α
S T : Submodule R A
⊢ span R (a • ↑S * ↑T) = span R (a • (↑S * ↑T))

Tactic:
smul_mul_assoc

Goal state after:
ι : Sort uι
R : Type u
inst✝⁶ : CommSemiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
S✝ T✝ : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst✝³ : Monoid α
inst✝² : DistribMulAction α A
inst✝¹ : SMulCommClass α R A
inst✝ : IsScalarTower α A A
a : α
S T : Submodule R A
⊢ span R (a • (↑S * ↑T)) = span R (a • (↑S * ↑T))
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
K : Ideal S
inst✝ : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ comap f K

Tactic:
rw [mem_comap, map_one]

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
K : Ideal S
inst✝ : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ K
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
⊢ a * b / b = a

Tactic:
refine (eq_of_sub_eq_zero ?_).symm
    by_contra h
    have := mul_right_not_lt b h
    rw [sub_mul, mul_comm (_ / _), sub_eq_iff_eq_add'.2 (div_add_mod (a * b) b).symm] at this
    exact this (mod_lt _ hb)

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

Goal state before:
pp: R : Type u_1
inst✝ : EuclideanDomain R
a b : R
⊢ b * (a / b) + a % b - b * (a / b) = a - b * (a / b)

Tactic:
by rw [div_add_mod]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p

Tactic:
rw [hq, zero_dvd_iff] at hpq
    rw [hpq]
    exact dvd_zero _

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ y ∣ z * gcdA x y

Tactic:
apply hyz.mul_right

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 : I ⊔ J = ⊤
⊢ I * K ⊔ J = K ⊔ J

Tactic:
rw [sup_comm] at h
  rw [sup_comm, sup_mul_eq_of_coprime_left h, sup_comm]

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun x ↦ s.gcd * x) (pmap f s ⋯)

Tactic:
rw [map_pmap]
        conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
        congr with (x hx)
        rw [id, ← hf hx]

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

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
⊢ s = map (fun x ↦ s.gcd * x) (pmap f s ⋯)

Tactic:
rw [map_pmap]
        conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
        congr with (x hx)
        rw [id, ← hf hx]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a

Tactic:
apply Iff.trans Multiset.lcm_dvd
  simp only [Multiset.mem_map, and_imp, exists_imp]
  exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
u : αˣ
a✝ : Nontrivial α
⊢ normalize a = normalize (a * ↑u)

Tactic:
refine by_cases (by rintro rfl; simp only [zero_mul]) fun ha : a ≠ 0 ↦ ?_

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
x y a b : R
e : a * x + b * y = 1
⊢ ∃ a b, y ∣ b ∧ a * x + b = 1

Tactic:
exact ⟨a, _, ⟨b, rfl⟩, mul_comm y b ▸ e⟩

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}

Tactic:
← IsBezout.span_gcd,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ Ideal.span {gcd x y} = Ideal.span {IsBezout.gcd x y}
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✝¹ : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
by
  have := nontrivial_of_invariantBasisNumber R
  have := basis_finite_of_finite_spans w.toFinite s b
  cases nonempty_fintype ι
  rw [Cardinal.mk_fintype ι]
  simp only [Nat.cast_le]
  exact Basis.le_span'' b s

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

Goal state before:
pp: case neg
ι : 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 b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : ¬f b ≤ f i
Hi : ¬I ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
have : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i := by
      simp only [hp.1.inf_le, hp.1.inf_le', not_or]
      exact ⟨⟨⟨Hi, Ha⟩, Hb⟩, Ht⟩

Goal state after:
case neg
ι : 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 b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : ¬f b ≤ f i
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
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
h : 0 < Module.rank R M
⊢ ¬Subsingleton M

Tactic:
intro h'

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
h : 0 < Module.rank R M
h' : Subsingleton M
⊢ False
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : 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 ∈ s, I ≤ f i

Tactic:
obtain ⟨t, hbt, rfl⟩ : ∃ t, b ∉ t ∧ insert b t = s :=
          ⟨s.erase b, Finset.notMem_erase b s, Finset.insert_erase hbs⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f b : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ diagonal (a • fun x ↦ 1) = diagonal fun x ↦ a

Tactic:
Pi.smul_def,

Goal state after:
m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ (diagonal fun i ↦ a • 1) = diagonal fun x ↦ a
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ diagonal (MulOpposite.op a • fun x ↦ 1) = diagonal fun x ↦ a

Tactic:
Pi.smul_def,

Goal state after:
m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ (diagonal fun i ↦ MulOpposite.op a • 1) = diagonal fun x ↦ a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∉ I → b ∈ I ^ n

Tactic:
intro ha

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
⊢ b ∈ I ^ n
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
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
⊢ M.submatrix e₁ id * N.submatrix (⇑e₂) id = M.submatrix e₁ ⇑e₂.symm * N

Tactic:
by
  ext; simp [mul_apply, ← e₂.bijective.sum_comp]

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
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → p
e₂ : o ≃ n
⊢ M.submatrix id ⇑e₂ * N.submatrix id e₁ = M * N.submatrix (⇑e₂.symm) e₁

Tactic:
by
  ext; simp [mul_apply, ← e₂.bijective.sum_comp]

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

Goal state before:
pp: ι : Type u_3
s : Finset ι
n : ℕ
⊢ toMultiset (∑ i ∈ s, single i n) = n • s.val

Tactic:
toMultiset_sum,

Goal state after:
ι : Type u_3
s : Finset ι
n : ℕ
⊢ ∑ i ∈ s, toMultiset (single i n) = n • s.val
Module: Mathlib.Data.Set.UnionLift

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

Tactic:
conv_lhs => rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]

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

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

Tactic:
by
  by_cases H : Module.Finite R S
  · have := Module.Finite.trans (R := R) S T
    exact finrank_bot_le_finrank_of_isScalarTower R S T
  · rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
    · exact zero_le
    · rwa [← not_lt, Module.rank_lt_aleph0_iff]

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
⊢ Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ (↑S ∪ ↑T)) =
    Subsemiring.closure (↑S.toSubsemiring ∪ ↑T.toSubsemiring)

Tactic:
Subalgebra.coe_toSubsemiring

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ (↑S ∪ ↑T)) = Subsemiring.closure (↑S ∪ ↑T)
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
s : Set A
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
this : ∃ z r, ∃ (_hr : r ∈ Submonoid.closure s), z • r = hd.prod
⊢ hd.prod ∈ span R ↑(Submonoid.closure s)

Tactic:
rcases this with ⟨z, r, hr, hzr⟩
      rw [← hzr]
      exact smul_mem _ _ (subset_span hr)

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ (x * y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ x *
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ y

Tactic:
dsimp
          apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
          all_goals simp

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
x : M →ₗ[R] N
⊢ lTensor P (rTensor Q x) ∘ₗ ↑(assoc R P M Q) = ↑(assoc R P N Q) ∘ₗ rTensor Q (lTensor P x)

Tactic:
by
  simp_rw [rTensor, lTensor, map_map_comp_assoc_eq]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
x : M →ₗ[R] N
⊢ map (map id x) id ∘ₗ ↑(assoc R P M Q).symm = ↑(assoc R P N Q).symm ∘ₗ map id (map x id)

Tactic:
map_map_comp_assoc_symm_eq

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p ↦ Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
⊢ (f ∘ₗ φ ∘ₗ s) p = g ((linearCombination R id) (s p))

Tactic:
simp [φ, Finsupp.linearCombination_apply, Function.surjInv_eq hf, map_finsuppSum]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ star (star x * y) = star y * x

Tactic:
rw [star_mul, star_star]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ star (x * star y) = y * star x

Tactic:
rw [star_mul, star_star]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : StarAddMonoid R
x : R
inst✝ : IsStarNormal x
⊢ -star x * -x = -x * -star x

Tactic:
neg_mul_neg,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : StarAddMonoid R
x : R
inst✝ : IsStarNormal x
⊢ star x * x = x * star x