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

Goal state before:
pp: case h
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}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
⊢ ∀ x ∈ t,
    (if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
      v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)

Tactic:
intro x hx

Goal state after:
case h
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}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
    v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)
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
x✝¹ : 1 ∉ I ∧ 1 ∉ J
x✝ : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ (1, 0) ∉ I.prod J

Tactic:
by simp [hI]

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
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
inst✝ : Finite M
s : Submodule R M
⊢ Submodule.span R ↑s = s

Tactic:
Submodule.span_eq

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
inst✝ : Finite M
s : Submodule R M
⊢ s = s
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 : x✝ ∈ span R' s
a✝ : x✝ • n ∈ s • N
⊢ (a✝¹ • x✝) • n ∈ s • N

Tactic:
rw [mem_span_set] at hr
          obtain ⟨c, hc, rfl⟩ := hr
          rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]
          refine Submodule.sum_mem _ fun i hi => ?_
          rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]
          exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn

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

Goal state before:
pp: case inl
R : Type u
inst✝ : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0

Tactic:
simp only [div_zero, dvd_zero]

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

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
⊢ 1 ∈ J

Tactic:
classical
  convert!
    J.add_mem (J.mul_mem_left (update 0 i r) hxJ) (b := update 1 i y)
      (le <| by apply update_self i y 1 ▸ hy)
  ext j
  obtain rfl | ne := eq_or_ne j i
  · simpa [eq_comm] using eq
  · simp [update_of_ne ne]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ comap f (map f (I • comap f p)) ≤ I • comap f p

Tactic:
rw [Submodule.comap_map_eq_of_injective hf]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m : M
hm : m ∈ span R T
x✝¹ : R
x✝ : x✝¹ ∈ Ideal.span S
⊢ x✝¹ • 0 ∈ span R (S • T)

Tactic:
rw [smul_zero]

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m : M
hm : m ∈ span R T
x✝¹ : R
x✝ : x✝¹ ∈ Ideal.span S
⊢ 0 ∈ span R (S • T)
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'
⊢ annihilator R (M × M') = annihilator R M ⊓ annihilator R M'

Tactic:
ext
  simp_rw [Ideal.mem_inf, mem_annihilator,
    Prod.forall, Prod.smul_mk, Prod.mk_eq_zero, forall_and_left, ← forall_and_right]

Goal state after:
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
x✝¹ : R
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ • 0 = 0

Tactic:
rw [smul_zero]

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

Goal state before:
pp: case mpr.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ x ∈ s, r • x = 0

Tactic:
intro x hx

Goal state after:
case mpr.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x : M
hx : x ∈ s
⊢ r • x = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
I : Ideal R
f : F
⊢ map f I ≤ ⊥ ↔ I ≤ comap f ⊥

Tactic:
map_le_iff_le_comap

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
I : Ideal R
f : F
⊢ I ≤ comap f ⊥ ↔ I ≤ comap f ⊥
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
r : R
I : Ideal R
f : R →+* S
⊢ map f (r • I) = f r • map f I

Tactic:
by
  rw [← Submodule.ideal_span_singleton_smul, smul_eq_mul, Ideal.map_mul, Ideal.map_span,
    Set.image_singleton, ← smul_eq_mul, Submodule.ideal_span_singleton_smul]

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd
⊢ (map (fun x ↦ a * x) (b ::ₘ s)).gcd = normalize a * (b ::ₘ s).gcd

Tactic:
map_cons,

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd
⊢ (a * b ::ₘ map (fun x ↦ a * x) s).gcd = normalize a * (b ::ₘ s).gcd
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : Associated (map (fun x ↦ a * x) s).gcd (a * s.gcd)
⊢ Associated (map (fun x ↦ a * x) (b ::ₘ s)).gcd (a * (b ::ₘ s).gcd)

Tactic:
map_cons,

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : Associated (map (fun x ↦ a * x) s).gcd (a * s.gcd)
⊢ Associated (a * b ::ₘ map (fun x ↦ a * x) s).gcd (a * (b ::ₘ s).gcd)
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:
← dvd_mul_right

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
⊢ gcd m n ∣ gcd m n
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
← dvd_mul_right

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
⊢ gcd m n ∣ gcd m n
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : CommMonoidWithZero α
n : α
a✝ : GCDMonoid α
H : 0 ∣ 0 * n
⊢ ∃ a₁ a₂, a₁ ∣ 0 ∧ a₂ ∣ n ∧ 0 = a₁ * a₂

Tactic:
exact ⟨0, n, dvd_refl 0, dvd_refl n, by simp⟩

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
a✝ : GCDMonoid α
h0 : ¬gcd k m = 0
⊢ ∃ a₁ a₂, a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
obtain ⟨a, ha⟩ := gcd_dvd_left k m
      refine ⟨gcd k m, a, gcd_dvd_right _ _, ?_, ha⟩
      rw [← mul_dvd_mul_iff_left h0, ← ha]
      exact dvd_gcd_mul_of_dvd_mul H

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (I ^ (n + 2)).radical = I.radical

Tactic:
by rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h_1 : ¬a * d = 0
h0 : lcm c (a * d) ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)

Tactic:
rw [mul_eq_zero] at ‹a * d ≠ 0›

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h_1 : ¬(a = 0 ∨ d = 0)
h0 : lcm c (a * d) ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hI : IsPrincipal I
⊢ Ideal.map f I = Ideal.map f (Ideal.span {generator I})

Tactic:
Ideal.span_singleton_generator

Goal state after:
R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hI : IsPrincipal I
⊢ Ideal.map f I = Ideal.map f I
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
⊢ (if a = 0 ∧ b = 0 then 0 else 1) ∣ a

Tactic:
simp +contextual

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

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
⊢ (if a = 0 ∧ b = 0 then 0 else 1) ∣ b

Tactic:
simp +contextual

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

Goal state before:
pp: case inr.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
hs : range ⇑v ⊆ ⋃ j, S' j
IJ : #↑J < #↑(range ⇑v)
⊢ (sum fun x ↦ ℵ₀) < #↑(range ⇑v)

Tactic:
· simpa

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 → α
i✝ j✝ : n
| (if i✝ = j✝ then d i✝ else 0) ∈ S

Tactic:
rw [ite_mem]

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
i✝ j✝ : n
| (i✝ = j✝ → d i✝ ∈ S) ∧ (¬i✝ = j✝ → 0 ∈ S)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : LinearIndependent R ⇑b
⊢ LinearIndependent R fun i ↦ b i • a

Tactic:
Fintype.linearIndependent_iff

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i, g i • b i = 0 → ∀ (i : n), g i = 0
⊢ ∀ (g : n → R), ∑ i, g i • b i • a = 0 → ∀ (i : n), g i = 0
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
inj : Injective ⇑f
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
have ⟨g, hg⟩ := f.exists_finsupp_nat_of_fin_fun_injective inj

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
inj : Injective ⇑f
g : (ℕ →₀ R) →ₗ[R] Fin n → R
hg : Injective ⇑g
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
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:
rcases s.eq_empty_or_nonempty with rfl | hsne

Goal state after:
case neg.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
hp : ∀ i ∈ ∅, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑∅, ↑(f i)
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ i ∈ ∅, I ≤ f i

case neg.inr
ι : 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
hsne : s.Nonempty
⊢ ∃ i ∈ s, I ≤ f i
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
i✝ : m
j✝ : n
| (if i = i✝ ∧ j = j✝ then a else 0) ∈ S

Tactic:
rw [ite_mem]

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
i✝ : m
j✝ : n
| (i = i✝ ∧ j = j✝ → a ∈ S) ∧ (¬(i = i✝ ∧ j = j✝) → 0 ∈ S)
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
obtain ⟨c, i, hi, hc⟩ := exists_inv_pow I ha n

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
⊢ b ∈ I ^ n
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : Pi.single i 1 ᵥ* M ^ k = 0
h' : l = k + (l - k)
⊢ Pi.single i 1 ᵥ* M ^ l = 0

Tactic:
h',

Goal state after:
n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : Pi.single i 1 ᵥ* M ^ k = 0
h' : l = k + (l - k)
⊢ Pi.single i 1 ᵥ* M ^ (k + (l - k)) = 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single i 1 = 0
h' : l = l - k + k
⊢ M ^ l *ᵥ Pi.single i 1 = 0

Tactic:
h',

Goal state after:
n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : M ^ k *ᵥ Pi.single i 1 = 0
h' : l = l - k + k
⊢ M ^ (l - k + k) *ᵥ Pi.single i 1 = 0
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι✝ : Type v
β : ι✝ → Type w
inst✝² : (i : ι✝) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x✝ : ⨁ (x : ι), M
p : ι
x : M
⊢ (of (fun x ↦ M) p) ((AddMonoidHom.id M) x) = (of (fun i ↦ M) p) x

Tactic:
AddMonoidHom.id_apply

Goal state after:
ι✝ : Type v
β : ι✝ → Type w
inst✝² : (i : ι✝) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x✝ : ⨁ (x : ι), M
p : ι
x : M
⊢ (of (fun x ↦ M) p) x = (of (fun i ↦ M) p) x
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ x = (DirectSum.id M ι).symm (x default)

Tactic:
id_symm_apply,

Goal state after:
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ x = (of (fun i ↦ M) default) (x default)
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
S : Subalgebra R R
⊢ S = default

Tactic:
refine le_antisymm ?_ bot_le

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.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ sSup (A '' {i, j}) = sSup {A i, A j}

Tactic:
Set.image_insert_eq,

Goal state after:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ sSup (insert (A i) (A '' {j})) = sSup {A i, A j}
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
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep A ∧ sSup (A '' {i, j}) = ⊤ ↔ IsCompl (A i) (A j)

Tactic:
Set.image_insert_eq,

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
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep A ∧ sSup (insert (A i) (A '' {j})) = ⊤ ↔ IsCompl (A i) (A j)
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
⊢ (IsInternal fun i ↦ A ↑i) ↔ IsInternal A

Tactic:
by
  simp [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top]

Goal state after:
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✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst✝² : SMul X R
inst✝¹ : SMul X A
inst✝ : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ ↑(((algebraMap R ↥S) (x • 1) * s) • t) = ↑((algebraMap R ↥T) (x • 1) * s • t)

Tactic:
apply mul_assoc

Goal state after:
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 : Set A
⊢ centralizer R s.centralizer.centralizer = centralizer R s

Tactic:
by
  apply SetLike.coe_injective
  simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

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

Goal state before:
pp: case a
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ (adjoin R s).toSubmodule ≤ span R ↑(Subsemigroup.closure s)

Tactic:
intro x hx

Goal state after:
case a
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
hx : x ∈ (adjoin R s).toSubmodule
⊢ x ∈ span R ↑(Subsemigroup.closure s)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
hf i k hik,

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ ((f k).comp (inclusion hik)) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ comap f (map f S) ≤ S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
intro x hx

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : x ∈ comap f (map f S)
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
⊢ Projective S N

Tactic:
obtain ⟨f, hf⟩ := ‹Projective R M›

Goal state after:
R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
⊢ Projective S N