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

Goal state before:
pp: case inr.inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 = ↑m
⊢ (x, y) ∈ r

Tactic:
convert! connect_next

Goal state after:
case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 = ↑m
⊢ x = a

case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 = ↑m
⊢ y = p.toFun i.succ
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ (p.smash q h).toFun (Fin.natAdd p.length i).castSucc = q.toFun i.castSucc

Tactic:
by
  dsimp only [smash, Fin.castSucc_natAdd]
  apply Fin.addCases_right

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ height x ≤ height (f x)

Tactic:
by
  simp only [height_eq_iSup_last_eq]
  apply iSup₂_le
  intro p hlast
  apply le_iSup₂_of_le (p.map f hf) (by simp [hlast]) (by simp)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case succ
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n✝ : ℕ
⊢ height x = ↑(n✝ + 1) ↔ (n✝ + 1 = 0 ∨ ∃ y < x, height y = ↑(n✝ + 1) - 1) ∧ ∀ y < x, height y < ↑(n✝ + 1)

Tactic:
case succ n =>
    simp only [Nat.cast_add, Nat.cast_one, add_eq_zero, one_ne_zero, and_false, false_or]
    rw [height_eq_coe_add_one_iff]
    simp only [hfin, true_and]
    congr! 3
    rename_i y _
    cases height y <;> simp; norm_cast; lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ.refine_2
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
⊢ (t₁.smash t₃ H).toFun ∘ ⇑{ toFun := Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length), inj' := ⋯ } =
    { length := n + 1, toFun := s, step := h }.toFun

Tactic:
refine funext (Fin.lastCases ?_ fun j ↦ ?_)
      · convert! h₂; simpa using! RelSeries.last_smash ..
      convert! congr_fun ht j using 1
      simp [RelSeries.smash_castLE]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case right
α : Type u_1
inst✝ : Preorder α
n : ℕ
p : LTSeries α
hp : p.length = n + 1
hfin : ∀ (n : ℕ), ∃ p_1, RelSeries.last p_1 = RelSeries.last p ∧ p_1.length = n
⊢ ↑n ≤ height (RelSeries.eraseLast p).last

Tactic:
simpa [hp] using length_le_height_last (p := p.eraseLast)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝ : IsEmpty α
⊢ InfiniteDimensionalOrder α

pp: case inr
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝ : Nonempty α
⊢ InfiniteDimensionalOrder α

Tactic:
· simp [krullDim_eq_bot] at h

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝ : Nonempty α
⊢ InfiniteDimensionalOrder α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
⊢ ↑(LTSeries.longestOf α).length ≤ ↑(height (RelSeries.last (LTSeries.longestOf α)))

Tactic:
height

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
⊢ ↑(LTSeries.longestOf α).length ≤ ↑(⨆ p, ⨆ (_ : RelSeries.last p ≤ RelSeries.last (LTSeries.longestOf α)), ↑p.length)
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: 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
⊢ TensorProduct.comm R N M ≪≫ₗ TensorProduct.comm R M N = LinearEquiv.refl R (N ⊗[R] M)

Tactic:
apply LinearEquiv.toLinearMap_injective; ext; rfl

Goal state after:
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
r✝ : ℤ
m : M
p : P
r : ℕ
ih : (↑r • m) ⊗ₜ[R] p = m ⊗ₜ[R] (↑r • p)
⊢ ((↑r + 1) • m) ⊗ₜ[R] p = m ⊗ₜ[R] ((↑r + 1) • p)

Tactic:
by simpa [add_smul, tmul_add, add_tmul] using ih

Goal state after:
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✝¹⁰ : SMulCommClass R R' M
inst✝⁹ : SMulCommClass R R'' M
R'₂ : Type u_22
inst✝⁸ : Monoid R'₂
inst✝⁷ : DistribMulAction R'₂ M
inst✝⁶ : SMulCommClass R R'₂ M
inst✝⁵ : SMul R'₂ R'
inst✝⁴ : DistribMulAction R'₂ N
inst✝³ : DistribMulAction R' N
inst✝² : CompatibleSMul R R'₂ M N
inst✝¹ : CompatibleSMul R R' M N
inst✝ : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x : M ⊗[R] N
m : M
n : N
⊢ (s • r) • m ⊗ₜ[R] n = s • r • m ⊗ₜ[R] n

Tactic:
by rw [← tmul_smul, ← tmul_smul, ← tmul_smul, smul_assoc]

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
⊢ map (↑(opLinearEquiv R).symm) 1 = 1

Tactic:
← comap_equiv_eq_map_symm,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ comap (↑(opLinearEquiv R)) 1 = 1
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ᵐᵒᵖ
⊢ map (↑(opLinearEquiv R).symm) (M * N) = map (↑(opLinearEquiv R).symm) N * map (↑(opLinearEquiv R).symm) M

Tactic:
map_unop_mul

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

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

Tactic:
constructor
  · rintro ⟨a, ha : a ∈ p, rfl⟩; simpa [inv_mul_cancel_left₀ hx]
  · exact fun h ↦ ⟨_, h, by simp [mul_inv_cancel_left₀ hx]⟩

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
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ map (↑(opLinearEquiv R).symm) (M ^ n) = map (↑(opLinearEquiv R).symm) M ^ n

Tactic:
← comap_equiv_eq_map_symm,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ comap (↑(opLinearEquiv R)) (M ^ n) = map (↑(opLinearEquiv R).symm) M ^ 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
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ comap (↑(opLinearEquiv R)) (M ^ n) = map (↑(opLinearEquiv R).symm) M ^ n

Tactic:
← comap_equiv_eq_map_symm,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ comap (↑(opLinearEquiv R)) (M ^ n) = comap (↑(opLinearEquiv R)) M ^ n
Module: Mathlib.RingTheory.Ideal.Prod

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

Tactic:
by
  let : IsPrime (prod I (⊤ : Ideal R)) := isPrime_ideal_prod_top
  rw [← map_prodComm_prod]
  -- Note: couldn't synthesize the right instances without the `R` and `S` hints
  exact map_isPrime_of_equiv (RingEquiv.prodComm (R := S) (S := R))

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

Goal state before:
pp: case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ x✝ : R'
hr : ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x✝
a✝ : x✝ • n ∈ s • N
⊢ (a✝¹ • x✝) • n ∈ s • N

Tactic:
obtain ⟨c, hc, rfl⟩ := hr

Goal state after:
case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r ↦ r • mi) • n ∈ s • N
⊢ (a✝¹ • c.sum fun mi r ↦ r • mi) • n ∈ s • N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
rcf : RingHomClass F R S
inst✝ : Nontrivial S
f : F
⊢ ¬1 = 0

Tactic:
exact one_ne_zero

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
I J : Ideal R
inst✝ : I.IsTwoSided
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ I * J ≠ ⊥

Tactic:
Ne,

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
I J : Ideal R
inst✝ : I.IsTwoSided
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ ¬I * J = ⊥
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
obtain ⟨i', hi', k, hk, rfl⟩ := hi

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i' + k
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ I ≤ N.annihilator ↔ I • N = ⊥

Tactic:
by
  simp_rw [← le_bot_iff, smul_le, SetLike.le_def, mem_annihilator]; rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).gcd f = GCDMonoid.gcd (s.gcd f) (s₂.gcd f)
⊢ (insert a s ∪ s₂).gcd f = GCDMonoid.gcd ((insert a s).gcd f) (s₂.gcd f)

Tactic:
rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ Codisjoint I J

Tactic:
by
  rw [IsCoprime, codisjoint_iff]
  constructor
  · rintro ⟨x, y, hxy⟩
    rw [eq_top_iff_one]
    apply (show x * I + y * J ≤ I ⊔ J from
      sup_le (mul_le_right.trans le_sup_left) (mul_le_right.trans le_sup_right))
    rw [hxy]
    simp only [one_eq_top, Submodule.mem_top]
  · intro h
    refine ⟨1, 1, ?_⟩
    simpa only [one_eq_top, top_mul, Submodule.add_eq_sup]

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

Goal state before:
pp: α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
⊢ ∃ I, I.IsMaximal ∧ a ∈ I

Tactic:
rcases Ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩

Goal state after:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ ∃ I, I.IsMaximal ∧ a ∈ I
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ ¬↑a ≠ 0 ∨ (↑a)⁻¹ ∉ S ↔ ↑a = 0 ∨ (↑a)⁻¹ ∉ S

Tactic:
Ne,

Goal state after:
α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ ¬¬↑a = 0 ∨ (↑a)⁻¹ ∉ S ↔ ↑a = 0 ∨ (↑a)⁻¹ ∉ S
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * d₁ ^ k * a')

Tactic:
mul_comm b'

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (d₁ ^ k * b' * a')
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
s : Finset ι
a b : ι
hn : s.card = 0
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
rw [Finset.card_eq_zero] at hn

Goal state after:
case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
s : Finset ι
a b : ι
hn : s = ∅
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
a b : ι
h : ↑I ⊆ ↑(f a) ∪ ↑(f b)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ ∅, I ≤ f i

Tactic:
subset_union

Goal state after:
case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
a b : ι
h : I ≤ f a ∨ I ≤ f b
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ ∅, I ≤ f i
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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : u.card + 1 = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
⊢ i ∉ u

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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
⊢ j ∉ u

Tactic:
exacts [hiu, hju]

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
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ #ι ≤ #↑w

Tactic:
fapply card_le_of_injective'' (R := R)
  · apply Finsupp.linearCombination
    exact fun i ↦ Span.repr R w ⟨v i, s ▸ trivial⟩
  · intro f g h
    apply_fun linearCombination R ((↑) : w → M) at h
    simp only [linearCombination_linearCombination,
               Span.finsupp_linearCombination_repr] at h
    exact i h

Goal state after:
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

pp: case neg
ι : 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:
case neg
ι : 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
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
r : R
⊢ Ideal.span {r} ≠ ⊥ ↔ r ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
r : R
⊢ ¬Ideal.span {r} = ⊥ ↔ r ≠ 0
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ (b.repr (b i • 0)) i' = (single (i, j) 1) (i', j')

Tactic:
· simp [hi]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ (toMultiset 0).toFinset = support 0

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 → (toMultiset f).toFinset = f.support → (toMultiset (single a b + f)).toFinset = (single a b + f).support

Tactic:
· rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 → (toMultiset f).toFinset = f.support → (toMultiset (single a b + f)).toFinset = (single a b + f).support
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: case neg
n : Type u_3
α : Type u_11
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
hi : ¬i = j
⊢ 0 ≤ 1 i j

Tactic:
· simp [hi]

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

Goal state before:
pp: case h
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
this : u = c • LinearMap.id
d : R
hcd : c • LinearMap.id = d • LinearMap.id
⊢ d = c

Tactic:
LinearMap.ext_iff

Goal state after:
case h
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
this : u = c • LinearMap.id
d : R
hcd : ∀ (x : M), (c • LinearMap.id) x = (d • LinearMap.id) x
⊢ d = c
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ iSup A = ⊤

Tactic:
rw [AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, AddMonoidHom.mrange_eq_top]
  exact Function.Bijective.surjective h

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
⊢ ∀ (r : R),
    (algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
by intro r; rw [Algebra.algebraMap_eq_smul_one]; apply s.smul_mem _ h1

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

Goal state before:
pp: case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
exact Subalgebra.add_mem _

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

Goal state before:
pp: case algebraMap
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
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
r : R
⊢ f ((algebraMap R A) r) ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩

Goal state after:
case algebraMap
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
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
r : R
this : f 1 ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f ((algebraMap R A) r) ∈ adjoin R (⇑f '' (s ∪ {1}))