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

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✝ : Subsingleton M
z : M ⊗[R] N
⊢ ∀ (x y : M ⊗[R] N), x = 0 → y = 0 → x + y = 0

Tactic:
rintro _ _ rfl rfl

Goal state after:
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✝ : Subsingleton M
z : M ⊗[R] N
⊢ 0 + 0 = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

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✝ : Subsingleton N
z : M ⊗[R] N
⊢ ∀ (x y : M ⊗[R] N), x = 0 → y = 0 → x + y = 0

Tactic:
rintro _ _ rfl rfl

Goal state after:
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✝ : Subsingleton N
z : M ⊗[R] N
⊢ 0 + 0 = 0
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₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
⊢ (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m, 0)) = (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) 0

Tactic:
simp_rw [map_zero, FreeAddMonoid.lift_eval_of, map_zero]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M ⊗[R] N →ₗ[R] P
⊢ lift ((mk R M N).compr₂ f) = f

Tactic:
lift_compr₂ f,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M ⊗[R] N →ₗ[R] P
⊢ f ∘ₗ lift (mk R M N) = f
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
⊢ IsUnit a ↔ a ∈ R⁰

Tactic:
← isRegular_iff_mem_nonZeroDivisors,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
⊢ IsUnit a ↔ IsRegular a
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: case negSucc
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
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ (congr (f ^ (n + 1)) (g ^ (n + 1)))⁻¹ = congr (f ^ (n + 1))⁻¹ (g ^ (n + 1))⁻¹

Tactic:
exact congr_symm _ _

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

Goal state before:
pp: case refine_2
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ m • 0 ∈ M • N ⊔ M • P

pp: case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ ∀ (x y : A),
    x ∈ closure (↑N ∪ ↑P) →
      y ∈ closure (↑N ∪ ↑P) → m • x ∈ M • N ⊔ M • P → m • y ∈ M • N ⊔ M • P → m • (x + y) ∈ M • N ⊔ M • P

Tactic:
· apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem

Goal state after:
case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ ∀ (x y : A),
    x ∈ closure (↑N ∪ ↑P) →
      y ∈ closure (↑N ∪ ↑P) → m • x ∈ M • N ⊔ M • P → m • y ∈ M • N ⊔ M • P → m • (x + y) ∈ M • N ⊔ M • P
Module: Mathlib.Algebra.Order.Kleene

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

Tactic:
apply add_le_add_right (mul_left_mono h)

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ m • np ∈ M • N ⊔ M • P

Tactic:
refine closure_induction (motive := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)
    · rintro x (hx | hx)
      exacts [le_sup_left (a := M • N) (smul_mem_smul hm hx),
        le_sup_right (a := M • N) (smul_mem_smul hm hx)]
    · apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem
    · intro _ _ _ _ h1 h2; rw [smul_add]; exact add_mem h1 h2

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : ℤ
h : IsCoprime a b
⊢ IsCoprime ↑a ↑b

Tactic:
by
  rcases h with ⟨u, v, H⟩
  use u, v
  rw_mod_cast [H]
  exact Int.cast_one

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ map (↑RingEquiv.prodComm) (I.prod J) = J.prod I

Tactic:
refine Trans.trans (ideal_prod_eq _) ?_
  simp [map_map]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ gcd 0 b ∣ 0 ∧ gcd 0 b ∣ b

Tactic:
gcd_zero_left

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ b ∣ 0 ∧ b ∣ b
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a ∣ b
⊢ gcd 0 a = a

Tactic:
gcd_zero_left

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a ∣ b
⊢ a = a
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y x✝ s✝ t✝ s'✝ t'✝ : R
⊢ (x✝, s'✝, t'✝).1 = gcd 0 x✝

Tactic:
gcd_zero_left

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y x✝ s✝ t✝ s'✝ t'✝ : R
⊢ (x✝, s'✝, t'✝).1 = x✝
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ normalize 0 = 0

Tactic:
simp [normalize]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ normalize 1 = 1

Tactic:
simp [normalize]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
⊢ normalize ↑u = 1

Tactic:
simp [normalize]

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]

Goal state after:
case hab
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b ∣ a ∧ gcd a b ∣ c

case hba
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ a ∧ gcd a c ∣ b
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : CommSemiring R
inst✝¹ : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst✝ : (map ϕ N).IsPrincipal
x : M
hx : x ∈ N
⊢ generator (map ϕ N) ∣ ϕ x

Tactic:
rw [← mem_iff_generator_dvd, Submodule.mem_map]
  exact ⟨x, hx, rfl⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : CommMonoidWithZero α
x✝ : IsCancelMulZero α ∧ ∀ (a b : α), ∃ c, ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d
left✝ : IsCancelMulZero α
h : ∀ (a b : α), ∃ c, ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d
⊢ IsGCDMonoid α

Tactic:
classical exact ⟨gcdMonoidOfExistsLCM h⟩

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

Goal state before:
pp: case pos
ι : 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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
have h' : (I : Set R) ⊆ f a ∪ f i ∪ ⋃ j ∈ (↑t : Set ι), f j := by
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_assoc,
          Set.union_assoc (f a : Set R),
          Set.union_eq_self_of_subset_left Hb] at h
        exact h
      specialize ih hp.2 hn h'
      rcases ih with (ih | ih | ⟨k, hkt, ih⟩)
      · exact Or.inl ih
      · exact Or.inr (Or.inr ⟨i, Finset.mem_insert_self i t, ih⟩)
      · exact Or.inr (Or.inr ⟨k, Finset.mem_insert_of_mem hkt, ih⟩)

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

Goal state before:
pp: case pos
ι : 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
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
specialize ih hp.2 hn HI

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
ih : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
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
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
⊢ 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_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i, g i • b i = 0 → ∀ (i : n), g i = 0
⊢ ∀ (g : n → R), ∑ i, g i • b i • a = 0 → ∀ (i : n), g i = 0

Tactic:
intro g hg

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i, g i • b i = 0 → ∀ (i : n), g i = 0
g : n → R
hg : ∑ i, g i • b i • a = 0
⊢ ∀ (i : n), g i = 0
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
inst✝ : Module.Finite K ↥(span K s)
⊢ ∃ f, (∀ (i : Fin (finrank K ↥(span K s))), f i ∈ s) ∧ span K (range f) = span K s ∧ LinearIndependent K f

Tactic:
rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, hts, ht_card, ht_span, ht_indep⟩

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
inst✝ : Module.Finite K ↥(span K s)
t : Finset M
hts : ↑t ⊆ s
ht_card : t.card = finrank K ↥(span K s)
ht_span : span K ↑t = span K s
ht_indep : LinearIndepOn K id ↑t
⊢ ∃ f, (∀ (i : Fin (finrank K ↥(span K s))), f i ∈ s) ∧ span K (range f) = span K s ∧ LinearIndependent K f
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i j : n
⊢ 0 ≤ (A ^ m * A) i j

Tactic:
mul_apply

Goal state after:
case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i j : n
⊢ 0 ≤ ∑ j_1, (A ^ m) i j_1 * A j_1 j
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, (∑ x_1, v x_1 * A x_1 x) * w x = ∑ j, ∑ i, v i * A i j * w j

Tactic:
Finset.sum_mul

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I = ⊤
⊢ ⊤ = I * ⊤

Tactic:
mul_top,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I = ⊤
⊢ ⊤ = I
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ (finsuppTotal ι M I v) f = ∑ i, ↑(f i) • v i

Tactic:
rw [finsuppTotal_apply, Finsupp.sum_fintype]

Goal state after:
case h
ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ ∀ (i : ι), ↑0 • v i = 0
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq o
inst✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : i = i''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''

Tactic:
by_cases h₂ : j = j''

Goal state after:
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq o
inst✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : i = i''
h₂ : j = j''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''

case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq o
inst✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : i = i''
h₂ : ¬j = j''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq o
inst✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : ¬i = i''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''

Tactic:
by_cases h₂ : j = j''

Goal state after:
case pos
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq o
inst✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : ¬i = i''
h₂ : j = j''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''

case neg
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq o
inst✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : ¬i = i''
h₂ : ¬j = j''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
inst✝ : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ s.sup f + a = s.sup fun i ↦ f i + a

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_add']

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ Disjoint {a} f.support

Tactic:
rwa [Finset.disjoint_singleton_left]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y → I.ringCon (x - y) 0

Tactic:
intro h; convert! I.ringCon.sub h (I.ringCon.refl y); abel

Goal state after: