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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x : α), IsMin x

Tactic:
by
  simp only [krullDim_nonpos_iff_forall_isMax, IsMax, IsMin]
  exact forall_comm

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α = ↑(⨆ p, ↑p.length)

Tactic:
by
  simp [krullDim, WithBot.coe_iSup (OrderTop.bddAbove _), WithBot.coe_natCast]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = x), ↑p.length + 1 ≤ height ↑x

Tactic:
apply iSup₂_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height ↑x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin p.length
⊢ ((p.toFun i.castSucc).untop ⋯, (p.toFun i.succ).untop ⋯) ∈ {(a, b) | a < b}

Tactic:
simpa [WithTop.untop_lt_iff, WithTop.coe_untop] using p.step i

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: n : ℕ∞
⊢ height n = n

Tactic:
cases n with

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑p.length ≤ (↑m + 1) * ↑n' + (↑m + 1 + ↑m)
⊢ False

Tactic:
← add_assoc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑p.length ≤ (↑m + 1) * ↑n' + (↑m + 1) + ↑m
⊢ False
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
n : ℕ∞
h' : height (f x) = n
⊢ height x ≤ (↑m + 1) * n + ↑m

Tactic:
cases n with

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

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

pp: case insert.mp.refine_1.inr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ update g i x j ∈ f j

Tactic:
· rwa [Function.update_self]

Goal state after:
case insert.mp.refine_1.inr
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ update g i x j ∈ f j
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
hr : r ∈ s
a : M
ha : a ∈ x
b : M
hb : b ∈ y
⊢ r • (a + b) ∈ s • x + s • y

Tactic:
rw [smul_add, add_eq_sup, Submodule.mem_sup]

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
hr : r ∈ s
a : M
ha : a ∈ x
b : M
hb : b ∈ y
⊢ ∃ y_1 ∈ s • x, ∃ z ∈ s • y, y_1 + z = r • a + r • b
Module: Mathlib.LinearAlgebra.TensorProduct.Map

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
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℤ
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)

Tactic:
cases n with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + b = b
hbc : b + c = c
⊢ a + (b + c) = b + c

Tactic:
← add_assoc,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + b = b
hbc : b + c = c
⊢ a + b + c = b + c
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b : α
⊢ a + (a + b) = a + b

Tactic:
← add_assoc,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b : α
⊢ a + a + b = a + b
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + c = c
hbc : b + c = c
⊢ a + (b + c) = c

Tactic:
hbc

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + c = c
hbc : b + c = c
⊢ a + c = c
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b : α
hbc : a ≤ b
c : α
⊢ a ⊔ c ≤ b ⊔ c

Tactic:
hbc

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b : α
hbc : a ≤ b
c : α
⊢ b ⊔ c ≤ b ⊔ c
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c a b : α
⊢ a + (a + b) = a + b

Tactic:
← add_assoc,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c a b : α
⊢ a + a + b = a + b
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
⊢ 0 * t ∈ ⨆ i, S i * T

Tactic:
by simp_rw [zero_mul]; apply zero_mem

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
⊢ ↑p ^ (n + 1) ⊆ ↑(p ^ (n + 1))

Tactic:
by rw [← Nat.succ_eq_add_one, coe_pow _ n.succ_ne_zero]

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

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

Tactic:
by
  rw [mul_comm] at h
  exact h.of_add_mul_left_left

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semifield R
m : R
⊢ IsCoprime m 0 ↔ m ≠ 0 ∨ 0 ≠ 0

Tactic:
simp [isCoprime_zero_right]

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

Goal state before:
pp: case mpr
m n : ℤ
⊢ m.gcd n = 1 → IsCoprime m n

Tactic:
rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]

Goal state after:
case mpr
m n : ℤ
⊢ m.gcdA n * m + m.gcdB n * n = 1 → ∃ a b, a * m + b * n = 1
Module: Mathlib.RingTheory.Coprime.Lemmas

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

Tactic:
by_cases hx : x = h.choose
          · rw [hx, Pi.single_eq_same, Pi.single_eq_same]
          · rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]

Goal state after:
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).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ n * M.toAddSubmonoid

Tactic:
cases n with

Goal state after:
Module: Mathlib.RingTheory.OrzechProperty

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this : Small.{max u ?u.51, v} M
⊢ Injective ⇑f

Tactic:
let := Equiv.addCommMonoid (equivShrink M).symm

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝ : Small.{max u ?u.51, v} M
this : AddCommMonoid (Shrink.{max u ?u.51, v} M) := (equivShrink M).symm.addCommMonoid
⊢ Injective ⇑f
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
inst✝ : RingHomClass F R S
I : Ideal S
h : I = ⊤
⊢ comap f I = ⊤

Tactic:
by rw [h, comap_top]

Goal state after:
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
inst✝ : RingHomClass F R S
ι : Type u_4
s : Finset ι
K : ι → Ideal S
⊢ comap f (s.inf K) = s.inf fun i ↦ comap f (K i)

Tactic:
by
  simp [Finset.inf_eq_iInf, comap_iInf]

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
⊢ Order.coheight (comap f I) = Order.coheight I

Tactic:
let φ := orderEmbeddingOfSurjective f hf

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := orderEmbeddingOfSurjective f hf
⊢ Order.coheight (comap f I) = Order.coheight I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
⊢ (comap f K).IsMaximal

Tactic:
by
  refine ⟨⟨comap_ne_top _ H.1.1, fun J hJ => ?_⟩⟩
  suffices map f J = ⊤ by
    have := congr_arg (comap f) this
    rw [comap_top, comap_map_of_surjective _ hf, eq_top_iff] at this
    rw [eq_top_iff]
    exact le_trans this (sup_le (le_of_eq rfl) (le_trans (comap_mono bot_le) (le_of_lt hJ)))
  refine
    H.1.2 (map f J)
      (lt_of_le_of_ne (le_map_of_comap_le_of_surjective _ hf (le_of_lt hJ)) fun h =>
        ne_of_lt hJ (_root_.trans (congr_arg (comap f) h) ?_))
  rw [comap_map_of_surjective _ hf, sup_eq_left]
  exact le_trans (comap_mono bot_le) (le_of_lt hJ)

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

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ (∃ q, q.IsPrime ∧ comap f q = p) → comap f (map f p) = p

Tactic:
rintro ⟨q, hq, rfl⟩
    simp

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ (∀ i ∈ ∅, x i ∈ I i) → ∏ i ∈ ∅, x i ∈ ∏ i ∈ ∅, I i

pp: case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i) →
        (∀ i ∈ insert a s, x i ∈ I i) → ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i

Tactic:
· grind [Submodule.mem_top]

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → Ideal R
x : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i) →
        (∀ i ∈ insert a s, x i ∈ I i) → ∏ i ∈ insert a s, x i ∈ ∏ i ∈ insert a s, I i
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ Associated (s.gcd fun x ↦ a * f x) (a * s.gcd f)

Tactic:
by
  classical exact s.induction_on (by simp) fun b s hbs h ↦ by
             simpa using .trans (.gcd .rfl h) (gcd_mul_left' ..)

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
hIJ : ¬I ⊔ J = ⊤
⊢ False

Tactic:
obtain ⟨P, hP, hIJ⟩ := Ideal.exists_le_maximal _ hIJ

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

Goal state before:
pp: case cons
ι : Type u_1
s✝ : Finset ι
f : ι → ℤ
a : ι
s : Finset ι
has : a ∉ s
ih : 0 ≤ s.gcd f
⊢ 0 ≤ (cons a s has).gcd f

Tactic:
rw [gcd_cons, ← Int.coe_gcd]

Goal state after:
case cons
ι : Type u_1
s✝ : Finset ι
f : ι → ℤ
a : ι
s : Finset ι
has : a ∉ s
ih : 0 ≤ s.gcd f
⊢ 0 ≤ ↑((f a).gcd (s.gcd f))
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
rintro x ⟨⟨n, rfl⟩, hx'⟩

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
h : y ∉ I
n : ℕ
hx' : (fun x ↦ y ^ x) n ∈ ↑I
⊢ (fun x ↦ y ^ x) n ∈ ⊥
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
have h1 : IsUnit (gcd (d₁ ^ k) b) := by
    apply isUnit_of_dvd_one
    trans gcd d₁ b ^ k
    · exact gcd_pow_left_dvd_pow_gcd
    · apply IsUnit.dvd
      apply IsUnit.pow
      apply isUnit_of_dvd_one
      grw [hd₁, hab.dvd]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ gcd x y * 1 = gcd (gcd x y * x') (gcd x y * y')

Tactic:
← ex,

Goal state after:
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ gcd x y * 1 = gcd x (gcd x y * y')
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
x y : G₀
x0 : x ≠ 0
y0 : y ≠ 0
⊢ ↑(if h : x * y = 0 then 1 else (Units.mk0 (x * y) h)⁻¹) =
    ↑((if h : x = 0 then 1 else (Units.mk0 x h)⁻¹) * if h : y = 0 then 1 else (Units.mk0 y h)⁻¹)

Tactic:
by simp [x0, y0, mul_comm]

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

Goal state before:
pp: 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 : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ (z * i + y) * x + i ^ (n + 1) = z * i * x + i * i ^ n + y * x

pp: 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 : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ z * i * x + i * i ^ n + y * x = 1

Tactic:
· ring

Goal state after:
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 : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ z * i * x + i * i ^ n + y * x = 1
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Mul α
inst✝¹ : Zero α
inst✝ : NoZeroDivisors α
a b : n → α
ha : a ≠ 0
hb : b ≠ 0
⊢ vecMulVec a b ≠ 0

Tactic:
intro h
  obtain ⟨i, ha⟩ := Function.ne_iff.mp ha
  obtain ⟨j, hb⟩ := Function.ne_iff.mp hb
  exact mul_ne_zero ha hb congr($h i j)

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

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

Tactic:
or_comm

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ b ∈ I ∨ a ∈ I ^ n
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
u : l → α
v w : m → α
x : n → α
⊢ vecMulVec u v * vecMulVec w x = vecMulVec u ((v ⬝ᵥ w) • x)

Tactic:
rw [vecMulVec_mul, vecMul_vecMulVec]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ ((diagonal fun x ↦ 1) *ᵥ v) x✝ = v x✝

Tactic:
mulVec_diagonal,

Goal state after:
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ 1 * v x✝ = v x✝
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_3
inst✝² : LinearOrder M
inst✝¹ : Add M
inst✝ : AddRightMono M
a : WithBot M
f : ι → M
⊢ fold max ⊥ (fun i ↦ ↑(f i) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a

Tactic:
simp [*, max_add_add_right]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case insert
ι : Type u_1
M : Type u_3
inst✝² : LinearOrder M
inst✝¹ : Add M
inst✝ : AddRightMono M
a : WithBot M
f : ι → M
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : fold max ⊥ (fun i ↦ ↑(f i) + a) s✝ = fold max ⊥ (WithBot.some ∘ f) s✝ + a
⊢ fold max ⊥ (fun i ↦ ↑(f i) + a) (insert a✝² s✝) = fold max ⊥ (WithBot.some ∘ f) (insert a✝² s✝) + a

Tactic:
simp [*, max_add_add_right]

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Type u_2
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⟩
T : Set α
hT : T ⊆ iUnion S
t : Set β
⊢ iUnionLift S f hf T hT ⁻¹' t = inclusion hT ⁻¹' ⋃ i, inclusion ⋯ '' f i ⁻¹' t

Tactic:
ext x
  simp only [mem_preimage, mem_iUnion, mem_image]
  constructor
  · rcases mem_iUnion.1 (hT x.prop) with ⟨i, hi⟩
    refine fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩
    rwa [iUnionLift_of_mem x hi] at h
  · rintro ⟨i, ⟨y, hi⟩, h, hxy⟩
    obtain rfl : y = x := congr_arg Subtype.val hxy
    rwa [iUnionLift_of_mem x hi]

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
cond : finrank R M = finrank R M'
⊢ lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')

Tactic:
simp only [← finrank_eq_rank, cond, lift_natCast]

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

Goal state before:
pp: case pos
R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
H : Module.Finite S M
⊢ finrank S M ≤ finrank R M

Tactic:
have := Module.Finite.trans (R := R) S M

Goal state after:
case pos
R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
H : Module.Finite S M
this : Module.Finite R M
⊢ finrank S M ≤ finrank R M
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
⊢ Function.Injective fun t ↦ {r | t.ringCon r 0}

Tactic:
rintro ⟨t₁⟩ ⟨t₂⟩ (h : {x | _} = {x | _})
    congr 1
    refine RingCon.ext fun a b ↦ ⟨fun H ↦ ?_, fun H ↦ ?_⟩
    · have H' : a - b ∈ {x | t₁ x 0} := sub_self b ▸ t₁.sub H (t₁.refl b)
      rw [h] at H'
      convert! t₂.add H' (t₂.refl b) using 1 <;> abel
    · have H' : a - b ∈ {x | t₂ x 0} := sub_self b ▸ t₂.sub H (t₂.refl b)
      rw [← h] at H'
      convert! t₁.add H' (t₁.refl b) using 1 <;> abel

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
⊢ ↑(-↑i - 1) ∈ S

Tactic:
Int.cast_sub,

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