mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (z * y - x) y ↔ IsRelPrime x y

Tactic:
sub_eq_neg_add,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (-x + z * y) y ↔ IsRelPrime x y
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
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ p x hx

Tactic:
refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H

Goal state after:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ ∃ (x_1 : x ∈ I • N), p x x_1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
⊢ (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
⊢ span (s ×ˢ t) ≤ (span s).prod (span t)

Tactic:
ideal_prod_eq (span (s ×ˢ t)),

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
⊢ (map (RingHom.fst R S) (span (s ×ˢ t))).prod (map (RingHom.snd R S) (span (s ×ˢ t))) ≤ (span s).prod (span t)
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hst : s.Nonempty ↔ t.Nonempty
⊢ span (s ×ˢ t) = (span s).prod (span t)

Tactic:
by
  simp_rw [iff_iff_and_or_not_and_not, Set.not_nonempty_iff_eq_empty] at hst
  obtain ⟨hs, ht⟩ | ⟨rfl, rfl⟩ := hst
  · conv_lhs => rw [Ideal.ideal_prod_eq (Ideal.span (s ×ˢ t))]
    congr 1
    · rw [Ideal.map_span]
      simp [Set.fst_image_prod _ ht]
    · rw [Ideal.map_span]
      simp [Set.snd_image_prod hs]
  · simp

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : P a b (xgcdAux a 1 0 b 0 1)
⊢ gcd a b = a * gcdA a b + b * gcdB a b

Tactic:
rwa [xgcdAux_val, xgcd_val] at this

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : R
⊢ (∀ (a : M) (b : M'), x✝ • a = 0 ∧ x✝ • b = 0) ↔ (∀ (m : M), x✝ • m = 0) ∧ ∀ (m : M'), x✝ • m = 0

Tactic:
forall_and_left,

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : R
⊢ (∀ (a : M), x✝ • a = 0 ∧ ∀ (x : M'), x✝ • x = 0) ↔ (∀ (m : M), x✝ • m = 0) ∧ ∀ (m : M'), x✝ • m = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ
R : Type u
inst✝¹ : Semiring R
s : R
inst✝ : (span {s}).IsTwoSided
n : ℕ
ih : span {s} ^ n = span {s ^ n}
⊢ span {s} ^ (n + 1) = span {s ^ (n + 1)}

Tactic:
| succ n ih =>

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:
grw [← bot_lt_iff_ne_bot, ← mul_le_inf, bot_lt_iff_ne_bot, Ne, mul_eq_bot]
  exact not_or_intro hI hJ

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

Goal state before:
pp: case succ
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : I.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
⊢ I ⊔ J ^ (n + 1) = ⊤

Tactic:
| succ n ih =>

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

Goal state before:
pp: α : 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

Tactic:
← s.map_id,

Goal state after:
α : 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
| map id s
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
⊢ I ⊔ J ^ (n + 1) = ⊤

Tactic:
| succ n ih =>

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1

Tactic:
choose f hf using @gcd_dvd _ _ _ s
      refine ⟨s.pmap @f fun _ ↦ id, ?_, extract_gcd' s _ h ?_⟩ <;>
      · 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.Nat

Goal state before:
pp: z : ℤ
h : z ≤ 0
⊢ normalize z = -z

Tactic:
obtain rfl | h := h.eq_or_lt
  · simp
  · rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : n ≠ 0 → ↑n = ⊤
hn : n + 1 ≠ 0
⊢ ↑(n + 1) = ⊤

Tactic:
| succ n ih =>

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
ι : Type u_2
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ ⨅ i, span {I i} = span {∏ i, I i}

Tactic:
rw [← Finset.inf_univ_eq_iInf, finset_inf_span_singleton]
  rwa [Finset.coe_univ, Set.pairwise_univ]

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

Goal state before:
pp: β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x ↦ f x * a) = s.gcd f * normalize a

Tactic:
simp_rw [mul_comm]; exact gcd_mul_left

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

Goal state before:
pp: case neg.refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
b : β
hb : b ∈ s
⊢ f b = s.gcd f * (fun b ↦ if hb : b ∈ s then g' hb else 0) b

Tactic:
simp only [hb, hg, dite_true]

Goal state after:
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
⊢ IsCoprime I J

Tactic:
rw [isCoprime_iff_sup_eq]
  by_contra hIJ
  obtain ⟨P, hP, hIJ⟩ := Ideal.exists_le_maximal _ hIJ
  exact h P (le_trans le_sup_left hIJ) (le_trans le_sup_right hIJ) hP.isPrime

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
⊢ gcd m n ∣ gcd (k * m) n

Tactic:
by
  grw [← dvd_mul_left]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
⊢ gcd m n ∣ gcd m (k * n)

Tactic:
by
  grw [← dvd_mul_left]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
⊢ Disjoint ↑(Submonoid.powers y) ↑I ↔ y ∉ I

Tactic:
refine ⟨fun h => Set.disjoint_left.1 h (Submonoid.mem_powers _),
      fun h => disjoint_iff.mpr (eq_bot_iff.mpr ?_)⟩

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
h : y ∉ I
⊢ ↑(Submonoid.powers y) ⊓ ↑I ⊆ ⊥
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ c = gcd a b * (e - f * d)

Tactic:
rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]

Goal state after:
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 b) ∪ (↑(f i) ∪ ⋃ 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_assoc,

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 a) ∪ ↑(f b) ∪ ↑(f i) ∪ ⋃ 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.PrincipalIdealDomain

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
⊢ 1 ∈ T

Tactic:
have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T
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 b) ∪ (↑(f i) ∪ ⋃ 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
Hb : f b ≤ f i
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)

Tactic:
← Set.union_assoc,

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 a) ∪ ↑(f b) ∪ ↑(f i) ∪ ⋃ 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
Hb : f b ≤ f i
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
this : Infinite ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
have w₂ := infinite_basis_le_maximal_linearIndependent' v' _ v.linearIndependent v.maximal

Goal state after:
case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
this : Infinite ι'
w₂ : lift.{w, w'} #ι' ≤ lift.{w', w} #ι
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
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
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
have := nontrivial_of_invariantBasisNumber R
  cases fintypeOrInfinite ι
  · -- `v` is a finite basis, so by `basis_finite_of_finite_spans` so is `v'`.
    -- haveI : Finite (range v) := Set.finite_range v
    have := basis_finite_of_finite_spans (Set.finite_range v) v.span_eq v'
    cases nonempty_fintype ι'
    -- We clean up a little:
    rw [Cardinal.mk_fintype, Cardinal.mk_fintype]
    simp only [Cardinal.lift_natCast, Nat.cast_inj]
    -- Now we can use invariant basis number to show they have the same cardinality.
    apply card_eq_of_linearEquiv R
    exact
      (Finsupp.linearEquivFunOnFinite R R ι).symm.trans v.repr.symm ≪≫ₗ v'.repr ≪≫ₗ
        Finsupp.linearEquivFunOnFinite R R ι'
  · -- `v` is an infinite basis,
    -- so by `infinite_basis_le_maximal_linearIndependent`, `v'` is at least as big,
    -- and then applying `infinite_basis_le_maximal_linearIndependent` again
    -- we see they have the same cardinality.
    have w₁ := infinite_basis_le_maximal_linearIndependent' v _ v'.linearIndependent v'.maximal
    rcases Cardinal.lift_mk_le'.mp w₁ with ⟨f⟩
    have : Infinite ι' := Infinite.of_injective f f.2
    have w₂ := infinite_basis_le_maximal_linearIndependent' v' _ v.linearIndependent v.maximal
    exact le_antisymm w₁ w₂

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : IsEmpty m
M N : Matrix m n α
⊢ M = N

Tactic:
ext i
    exact isEmptyElim i

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
⊢ diagonal d ∈ S.matrix ↔ ∀ (i : n), d i ∈ S

Tactic:
simp only [Set.mem_matrix, diagonal, of_apply]

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
⊢ (∀ (i j : n), (if i = j then d i else 0) ∈ S) ↔ ∀ (i : n), d i ∈ S
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
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)
⊢ False

Tactic:
rcases Set.not_subset.1 HI with ⟨s, hsI, hs⟩

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
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)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
⊢ False
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ
ι : 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
s : Finset ι
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
hn : s.card = n + 1
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
| succ n ih =>

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

Goal state before:
pp: case refine_1
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0

Tactic:
Matrix.mul_apply,

Goal state after:
case refine_1
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ ∑ j, A 0 j * B j 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case refine_2
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1

Tactic:
Matrix.mul_apply,

Goal state after:
case refine_2
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ ∑ j, A 0 j * B j 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case refine_3
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0

Tactic:
Matrix.mul_apply,

Goal state after:
case refine_3
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ ∑ j, A 1 j * B j 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inr.inl
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✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : g.symm j ≠ j'
⊢ single i j r (f (f.symm i)) (g j') = single (f.symm i) (g.symm j) r (f.symm i) j'

Tactic:
single_apply_of_col_ne _ _ hj,

Goal state after:
case inr.inl
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✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : g.symm j ≠ j'
⊢ single i j r (f (f.symm i)) (g j') = 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case refine_4
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
Matrix.mul_apply,

Goal state after:
case refine_4
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ ∑ j, A 1 j * B j 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
ih : ∃ y, y * x + i ^ n = 1
⊢ ∃ y, y * x + i ^ (n + 1) = 1

Tactic:
| succ n ih =>

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
x : Matrix n n α
⊢ x ∈ Set.center (Matrix n n α) ↔ x ∈ ⇑(scalar n) '' Set.center α

Tactic:
simp_rw [Set.mem_image, Semigroup.mem_center_iff]
  refine ⟨fun hx ↦ ?_, fun ⟨x, hx, eq⟩ y ↦ eq ▸ scalar_commute x (hx · |>.symm) y |>.symm⟩
  refine (isEmpty_or_nonempty n).elim (fun _ ↦ ⟨0, by simp [nontriviality]⟩) fun ⟨i⟩ ↦ ?_
  obtain ⟨x, rfl⟩ := mem_range_scalar_iff_commute_single'.mpr fun _ _ ↦ hx _
  exact ⟨x, by simpa using fun r ↦ congr($(hx (single i i r)) i i)⟩

Goal state after:
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 ι
f : ι → M
a : M
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ f i + a ≤ s.sup' hs f + a

Tactic:
grw [← Finset.le_sup' _ hi]

Goal state after:
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
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)

Tactic:
rcases dir i j with ⟨k, hik, hjk⟩

Goal state after:
α : 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
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
H' : a - b ∈ {x | t₂ x 0}
⊢ t₁ a b

Tactic:
rw [← h] at H'

Goal state after:
case refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
H' : a - b ∈ {x | { ringCon := t₁ }.ringCon x 0}
⊢ t₁ a b
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
S : Subalgebra R A
r : R
⊢ (e.toRingEquiv.subsemiringMap S.toSubsemiring).toFun ((algebraMap R ↥S) r) = (algebraMap R ↥(Subalgebra.map (↑e) S)) r

Tactic:
ext; exact e.commutes r

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Subring R
i✝ : ℤ
i : ℕ
ih : (algebraMap ℤ R) ↑i ∈ S.carrier
⊢ (algebraMap ℤ R) (↑i + 1) ∈ S.carrier

Tactic:
by simpa using S.add_mem ih S.one_mem

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ ((finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = p i • n

Tactic:
simp [finsuppScalarLeft]

Goal state after: