mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
x : A
hx : x ∈ M ^ n
⊢ C n x hx

Tactic:
induction n generalizing x with

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 (RingHom.fst R S) (I.prod J) = I

Tactic:
by
  ext x
  rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective]
  exact
    ⟨by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.1, fun h => ⟨⟨x, 0⟩, ⟨⟨h, Ideal.zero_mem _⟩, rfl⟩⟩⟩

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, n * y ∈ 1
⊢ n * m ∈ 1

Tactic:
exact hn m hm

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ I * (1 / I) ≤ 1

Tactic:
rw [Submodule.mul_le]
  intro m hm n hn
  rw [Submodule.mem_div_iff_forall_mul_mem] at hn
  rw [mul_comm]
  exact hn m hm

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : PEmpty.{u_6 + 1} → Submodule R N} [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
intros

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
M✝ : PEmpty.{u_6 + 1} → Submodule R N
inst✝ : ∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
intros

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

Goal state before:
pp: case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * s' - a * (b✝ / a✝ * s) + (b * t' - b * (b✝ / a✝ * t))

Tactic:
add_sub,

Goal state after:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * s' - a * (b✝ / a✝ * s) + b * t' - b * (b✝ / a✝ * t)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ P a b (a, 1, 0)

Tactic:
dsimp [P]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ P a b (b, 0, 1)

Tactic:
dsimp [P]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝ : EuclideanDomain R
n : ℕ
c : R
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / 0 ^ n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Goal state after:
case inl.inl
R : Type u_1
inst✝ : EuclideanDomain R
c : R
⊢ (0 * c / 0) ^ 0 = (0 * c) ^ 0 / 0 ^ 0

case inl.inr
R : Type u_1
inst✝ : EuclideanDomain R
n : ℕ
c : R
hn : n ≠ 0
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / 0 ^ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_3.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∀ (a : ι), 0 • f a = 0

Tactic:
intros

Goal state after:
case mp.refine_3.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
a✝ : ι
⊢ 0 • f a✝ = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_3.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∀ (a : ι) (b₁ b₂ : R), (b₁ + b₂) • f a = b₁ • f a + b₂ • f a

Tactic:
intros

Goal state after:
case mp.refine_3.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
a✝ : ι
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • f a✝ = b₁✝ • f a✝ + b₂✝ • f a✝
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i a ↦ (c * a) • f i) = a.sum fun a b ↦ c • b • f a

Tactic:
intros

Goal state after:
case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i a ↦ (c * a) • f i) = a.sum fun a b ↦ c • b • f a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ (i : ι), 0 • f i = 0

Tactic:
intros

Goal state after:
case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
i✝ : ι
⊢ 0 • f i✝ = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * lcm x y = x * y

Tactic:
by
  rw [lcm]; by_cases h : gcd x y = 0
  · rw [h, zero_mul]
    rw [EuclideanDomain.gcd_eq_zero_iff] at h
    rw [h.1, zero_mul]
  rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
  generalize gcd x y = g at h hr ⊢; subst hr
  rw [mul_assoc, mul_div_cancel_left₀ _ h]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
⊢ I ⊔ ⨅ i ∈ s, J i = ⊤

Tactic:
exact s.induction_on' (by simp) fun {i t} his hts hit eq_top ↦ top_unique <| by
    rw [Finset.iInf_insert, inf_comm]
    refine le_trans ?_ (sup_le_sup_left mul_le_inf _)
    simpa only [sup_mul_eq_of_coprime_right (h _ his)] using eq_top.ge

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : f x' ∈ sInf (map f '' A)
hx : f x = f x'
this : ∀ I ∈ A, f x' ∈ map f I
⊢ x - x' ∈ J

Tactic:
apply h J hJ

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : f x' ∈ sInf (map f '' A)
hx : f x = f x'
this : ∀ I ∈ A, f x' ∈ map f I
⊢ x - x' ∈ RingHom.ker f
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:
obtain rfl | hn := eq_or_ne n 0

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

case succ.inr
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
hn : n ≠ 0
⊢ I ⊔ J ^ (n + 1) = ⊤
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inr
a : ℤ
h : a = -↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a

Tactic:
· use -1, isUnit_one.neg
    rw [← neg_eq_iff_eq_neg.mpr h]
    simp only [neg_mul, one_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
⊢ map f I.radical = (map f I).radical

Tactic:
by
  rw [radical_eq_sInf, radical_eq_sInf]
  have : ∀ J ∈ {J : Ideal R | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J := fun J hJ => h.trans hJ.left
  convert! map_sInf hf this
  ext j
  constructor
  · rintro ⟨hj, hj'⟩
    have : j.IsPrime := hj'
    exact
      ⟨comap f j, ⟨⟨map_le_iff_le_comap.1 hj, comap_isPrime f j⟩, map_comap_of_surjective f hf j⟩⟩
  · rintro ⟨J, ⟨hJ, hJ'⟩⟩
    have : J.IsPrime := hJ.right
    exact ⟨hJ' ▸ map_mono hJ.left, hJ' ▸ map_isPrime_of_surjective hf (le_trans h hJ.left)⟩

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 β
⊢ s₂.lcm f = normalize (s₂.lcm f)

Tactic:
normalize_lcm

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ s₂.lcm f = s₂.lcm f
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : Nontrivial α
⊢ s.lcm f ≠ 0 ↔ ∀ x ∈ s, f x ≠ 0

Tactic:
simp [lcm_eq_zero_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ gcd a b = 0

Tactic:
rw [ha, hb, ← zero_dvd_iff]
    apply dvd_gcd <;> rfl

Goal state after:
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]
  have h2 : d₁ ^ k ∣ a * b := by
    use d₂ ^ k
    rw [h, hc]
    exact mul_pow d₁ d₂ k
  rw [mul_comm] at h2
  have h3 : d₁ ^ k ∣ a := by
    apply (dvd_gcd_mul_of_dvd_mul h2).trans
    rw [h1.mul_left_dvd]
  have h4 : d₁ ^ k ≠ 0 := by
    intro hdk
    rw [hdk] at h3
    apply absurd (zero_dvd_iff.mp h3) ha
  exact ⟨h4, h3⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
⊢ ((fun a ↦ span {a}) '' Set.univ).WellFoundedOn fun x1 x2 ↦ x1 > x2

Tactic:
Set.wellFoundedOn_image,

Goal state after:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
⊢ Set.univ.WellFoundedOn (Function.onFun (fun x1 x2 ↦ x1 > x2) fun a ↦ span {a})
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
⊢ a = 0 ∨ b = 0

Tactic:
have : Associated (a * b) 0 := (gcd_mul_lcm a b).symm.trans <| by rw [h, mul_zero]
      rwa [← mul_eq_zero, ← associated_zero_iff_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
h : IsRelPrime x y
⊢ IsUnit (gcd x y)

Tactic:
exact h (gcd_dvd_left x y) (gcd_dvd_right x y)

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

Goal state before:
pp: case i.hg
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ⇑↑b.repr

pp: case i.hf
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ⇑(Finsupp.linearCombination R Subtype.val)

Tactic:
· apply LinearEquiv.surjective

Goal state after:
case i.hf
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ⇑(Finsupp.linearCombination R Subtype.val)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq : Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
· rw [or_iff_not_imp_left, ← Ne, ← Cardinal.one_le_iff_ne_zero, one_le_rank_iff] at eq
    rw [← n.succ_pred_eq_of_pos pos] at eq ⊢
    exact eq ⟨.single R (fun _ ↦ _) 0, Pi.single_injective (M := fun _ ↦ _) _⟩

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

Tactic:
refine ⟨z * i + y, ?_⟩

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

Goal state before:
pp: case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ ∀ x ∈ Finset.univ ×ˢ Finset.univ, P (single x.1 x.2 (M x.1 x.2))

Tactic:
intros

Goal state after:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝¹ : Fintype m
val✝ : Fintype n
x✝ : m × n
a✝ : x✝ ∈ Finset.univ ×ˢ Finset.univ
⊢ P (single x✝.1 x✝.2 (M x✝.1 x✝.2))
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
⊢ A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y

Tactic:
ext
  apply dotProduct_sub

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
a✝ : α
⊢ (f ⊔ g) a✝ = max (f a✝) (g a✝)

Tactic:
Finsupp.sup_apply

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (∀ {x y : Mᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    c ≤ d

Tactic:
le_def

Goal state after:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (∀ {x y : Mᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    ∀ {x y : M}, c x y → d x y
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (∀ {x y : Rᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    c ≤ d

Tactic:
le_def

Goal state after:
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (∀ {x y : Rᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    ∀ {x y : R}, c x y → d x y
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
⊢ ∀ (a : Subalgebra R R), a = default

Tactic:
intro S

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S✝ : Subalgebra R A
S : Subalgebra R R
⊢ S = default
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubsemiring = T.toSubsemiring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
by rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
⊢ IsInternal fun i ↦ Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
refine (isInternal_submodule_iff_iSupIndep_and_iSup_eq_top _).mpr ⟨?_, by simp [iSup_subtype]⟩

Goal state after:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
⊢ iSupIndep fun i ↦ Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_11
inst✝¹ : Semiring S
inst✝ : Algebra R S
m : R ⊗[R] M
⊢ ∀ (m : M), (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m = 1 ⊗ₜ[R] m

Tactic:
intros

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_11
inst✝¹ : Semiring S
inst✝ : Algebra R S
m : R ⊗[R] M
m✝ : M
⊢ (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m✝ = 1 ⊗ₜ[R] m✝
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
⊢ ∀ (n : ℕ) (x : ↥(selfAdjoint R)), ↑(n • x) = n • ↑x

Tactic:
intros

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
n✝ : ℕ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
⊢ ∀ (n : ℤ) (x : ↥(selfAdjoint R)), ↑(n • x) = n • ↑x

Tactic:
intros

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
n✝ : ℤ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
⊢ ∀ (n : ℤ) (x : ↥(selfAdjoint R)), ↑(n • x) = n • ↑x

Tactic:
intros

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
n✝ : ℤ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
x✝ :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
⊢ A = B

Tactic:
← fromBlocks_toBlocks A,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
x✝ :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
⊢ fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ = B
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = diagonal (Function.update v i x) j k

Tactic:
· rw [diagonal_apply_ne _ hjk]
    obtain rfl | hki := eq_or_ne k i
    · rw [updateCol_self, Pi.single_eq_of_ne hjk]
    · rw [updateCol_ne hki, diagonal_apply_ne _ hjk]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : DecidableEq n
A : Matrix m n α
j : n
x y : m → α
⊢ (A.updateCol j x).updateCol j y = A.updateCol j y

Tactic:
simpa only [updateRow_transpose] using! congr_arg transpose <| updateRow_idem Aᵀ j x y

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

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
y z : OreLocalization S X
r₁ : X
s₁ : ↥S
⊢ r₁ /ₒ s₁ + y + z = r₁ /ₒ s₁ + (y + z)

Tactic:
induction y with | _ r₂ s₂

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ r₁ /ₒ s₁ + r₂ /ₒ s₂ + z = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + z)