mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
⊢ ⁅x_χ, m_α⁆ ∈ sl2SubmoduleOfRoot ⋯

Tactic:
have hx_χ_in_sl2 : x_χ ∈ sl2SubalgebraOfRoot hα₀ := by
      obtain ⟨h, e, f, ht, he, hf⟩ := exists_isSl2Triple_of_weight_isNonZero hα₀
      rw [mem_sl2SubalgebraOfRoot_iff hα₀ ht he hf]
      have hx_χ_neg : x_χ ∈ genWeightSpace L (-α.toLinear) := by
        rw [← (add_eq_zero_iff_eq_neg.mp w_plus)]
        exact hx_χ
      obtain ⟨c, hc⟩ := (finrank_eq_one_iff_of_nonzero' ⟨f, hf⟩ (by simp [ht.f_ne_zero])).mp
        (finrank_rootSpace_eq_one (-α) (by simpa using hα₀)) ⟨x_χ, hx_χ_neg⟩
      exact ⟨0, c, 0, by simpa using hc.symm⟩

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
hx_χ_in_sl2 : x_χ ∈ sl2SubalgebraOfRoot hα₀
⊢ ⁅x_χ, m_α⁆ ∈ sl2SubmoduleOfRoot ⋯
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ (auxInv S r).comp (auxHom S r).toRingHom = RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})

Tactic:
rw [← RingHom.cancel_right (Ideal.Quotient.mk_surjective)]

Goal state after:
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ((auxInv S r).comp (auxHom S r).toRingHom).comp (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) =
    (RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
      (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S ι σ
i : σ
⊢ P.relation i ∈ P.ker

Tactic:
← P.span_range_relation_eq_ker

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S ι σ
i : σ
⊢ P.relation i ∈ Ideal.span (Set.range P.relation)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Generators R T ι
s : T
⊢ (aeval P.val) ((MvPolynomial.map (algebraMap R S)) (P.σ s)) = s

Tactic:
by simp [@aeval_def S, ← IsScalarTower.algebraMap_eq, ← @aeval_def R]

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a.convert_4
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := ⋯
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := ⋯
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ (Q.toComp P).toAlgHom.toRingHom
      (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i, (monomial j.2) (coeff (e.symm j) x)) ∈
    Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker

Tactic:
refine Ideal.mem_map_of_mem _ ?_

Goal state after:
case a.convert_4
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i, (monomial j.2) (coeff (e.symm j) x) ∈ P.ker
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Odd ↑(2 * l + 1)

Tactic:
rw [val_add, val_mul, coe_ofNat_eq_mod, coe_ofNat_eq_mod]

Goal state after:
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Odd ((2 % (n + n) * ↑l % (n + n) + 1 % (n + n)) % (n + n))
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n ↦ ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (cast R M h) a.snd = b.snd
⊢ a = b

Tactic:
refine gradedMonoid_eq_of_reindex_cast h ?_
  rw [cast] at h2
  rw [← finCongr_eq_equivCast, ← h2]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
⊢ f ↑n * a' ↑n + ∑ i ∈ s, f i * a' i = ∑ i ∈ insert n✝ s, f i * a' i

Tactic:
s.sum_insert hn,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
⊢ f ↑n * a' ↑n + ∑ i ∈ s, f i * a' i = f n✝ * a' n✝ + ∑ i ∈ s, f i * a' i
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ (liftAux φ) ((tprod R) f) = φ f

Tactic:
simp only [liftAux, liftAddHom, tprod_eq_tprodCoeff_one, tprodCoeff, AddCon.coe_mk']

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ ((addConGen (Eqv R s)).lift (FreeAddMonoid.lift fun p ↦ p.1 • φ p.2) ⋯) ↑(FreeAddMonoid.of (1, f)) = φ f
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case insert.specialize_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i ∈ insert n✝ s, f i • v i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ ∑ i ∈ s, f i • (v + fun x ↦ c x • v ↑n) i = 0

Tactic:
s.sum_insert hn,

Goal state after:
case insert.specialize_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : f n✝ • v n✝ + ∑ x ∈ s, f x • v x = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ ∑ i ∈ s, f i • (v + fun x ↦ c x • v ↑n) i = 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := ⋯
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := ⋯
hn0 : n ≠ 0
hJ : I ^ n * J ≤ ann
K : Ideal R := ⋯
y : R
hy : y ∈ K
p : R
hp : p ∈ I
⊢ p * y ∈ I ^ n * J

Tactic:
simpa [K, ← mul_assoc, mul_pow_sub_one hn0] using mul_mem_mul hp hy

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R ((fun i ↦ ↑i) ∘ ![a, b])
i : Fin (Nat.succ 0).succ
⊢ ↑(![↑a, ↑b] i) = ↑(((fun i ↦ ↑i) ∘ ![a, b]) i)

Tactic:
fin_cases i <;> simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = (⊥.colon {(Ideal.Quotient.mkₐ R I) x}).radical
this : x ∉ I
h : ∀ {y : R}, y ∈ ⊥.colon {(Ideal.Quotient.mk I) x} ↔ y * x ∈ I
y : R
hy : y ∈ ⊥.colon {(Ideal.Quotient.mk I) x}
⊢ y ∈ (colon I Set.univ).radical

Tactic:
← Set.top_eq_univ

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e : J = (⊥.colon {(Ideal.Quotient.mkₐ R I) x}).radical
this : x ∉ I
h : ∀ {y : R}, y ∈ ⊥.colon {(Ideal.Quotient.mk I) x} ↔ y * x ∈ I
y : R
hy : y ∈ ⊥.colon {(Ideal.Quotient.mk I) x}
⊢ y ∈ (colon I ⊤).radical
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x, x ≠ 0 ∧ I' = Ideal.span {x}) → ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤

Tactic:
· rintro ⟨x, hx, rfl⟩
    exact ⟨1, x, one_ne_zero, hx, by rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]⟩

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: case mpr
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f✝ : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f✝ ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f✝)).range
f : LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N
⊢ f ∈
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
            (LocalizedModule I.primeCompl N))
          ((LocalizedModule.map I.primeCompl) f✝)).range →
    f ∈ Submodule.localized₀ I.primeCompl (LocalizedModule.map I.primeCompl) ((llcomp R N M N) f✝).range

Tactic:
rintro ⟨g, rfl⟩
      obtain ⟨⟨g, s⟩, rfl⟩ :=
        IsLocalizedModule.mk'_surjective I.primeCompl (LocalizedModule.map I.primeCompl) g
      simp only [Function.uncurry_apply_pair]
      refine ⟨f.comp g, ⟨g, rfl⟩, s, ?_⟩
      apply ((Module.End.isUnit_iff _).mp <| IsLocalizedModule.map_units
         (LocalizedModule.map I.primeCompl) s).injective
      simp only [Module.algebraMap_end_apply, ← Submonoid.smul_def, IsLocalizedModule.mk'_cancel',
        ← LinearMap.map_smul_of_tower]
      apply LinearMap.restrictScalars_injective R
      apply IsLocalizedModule.ext I.primeCompl (LocalizedModule.mkLinearMap I.primeCompl N)
      · exact IsLocalizedModule.map_units (LocalizedModule.mkLinearMap I.primeCompl N)
      ext
      simp only [coe_comp, coe_restrictScalars, Function.comp_apply,
        LocalizedModule.mkLinearMap_apply, LocalizedModule.map_mk, llcomp_apply]

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case refine_2
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsClosed[inst✝¹] ((fun x ↦ if x ∈ U then 0 else 1) ⁻¹' {1})ᶜ

Tactic:
convert! hU.1

Goal state after:
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ((fun x ↦ if x ∈ U then 0 else 1) ⁻¹' {1})ᶜ = U
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsLocallyConstant fun x ↦ if x ∈ U then 0 else 1

Tactic:
refine IsLocallyConstant.iff_isOpen_fiber.2 <| Fin.forall_fin_two.2 ⟨?_, ?_⟩
    · convert! hU.2 using 1
      ext
      simp only [mem_singleton_iff, Fin.one_eq_zero_iff, mem_preimage, ite_eq_left_iff,
        Nat.succ_succ_ne_one]
      tauto
    · rw [← isClosed_compl_iff]
      convert! hU.1
      ext
      simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S✝
inst✝⁶ : Algebra R S✝
S : Submonoid R
ι : Type u_3
inst✝⁵ : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → AddCommMonoid (M' i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → Module R (M' i)
f : (i : ι) → M i →ₗ[R] M' i
inst✝ : ∀ (i : ι), IsLocalizedModule S (f i)
⊢ IsLocalizedModule S (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)

Tactic:
let (i : ι) : Module (Localization S) (M' i) := IsLocalizedModule.module S (f i)
  rw [isLocalizedModule_iff_isBaseChange S (Localization S)]
  apply IsBaseChange.pi
  intro i
  rw [← isLocalizedModule_iff_isBaseChange S]
  infer_instance

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
⊢ (derivedSeries G n).Normal

Tactic:
induction n with
  | zero => exact (⊤ : Subgroup G).normal_of_characteristic
  | succ n ih => exact Subgroup.commutator_normal (derivedSeries G n) (derivedSeries G n)

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ ⁅H, H⁆ = ⁅H, H⁆.subtype.range

Tactic:
range_subtype

Goal state after:
case h.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ ⁅H, H⁆ = ⁅H, H⁆
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
⊢ IsOpen (freeLocus R M)

Tactic:
refine isOpen_iff_forall_mem_open.mpr fun x hx ↦ ?_
  have : Module.Free _ _ := hx
  obtain ⟨r, hr, hr', _⟩ := Module.FinitePresentation.exists_free_localizedModule_powers
    x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
    (Localization.AtPrime x.asIdeal)
  exact ⟨basicOpen r, basicOpen_subset_freeLocus_iff.mpr inferInstance, (basicOpen r).2, hr⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
h : rankAtStalk M = 0
⊢ support R M = ∅

Tactic:
Set.eq_empty_iff_forall_notMem

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
h : rankAtStalk M = 0
⊢ ∀ (x : PrimeSpectrum R), x ∉ support R M
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case right
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ ⨆ f, f.fieldRange = ⊤

Tactic:
← top_le_iff

Goal state after:
case right
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ ⊤ ≤ ⨆ f, f.fieldRange
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp.refine_1
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
⊢ ∃ b, (↑e 1).1 * b = 1

Tactic:
have : span R {(e 1).1 * e' 1} = 1 := by simpa [span_mul_span] using congr($h * $h').symm

Goal state after:
case mp.refine_1
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
this : R ∙ ↑(e 1) * ↑(e' 1) = 1
⊢ ∃ b, (↑e 1).1 * b = 1
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
obtain ⟨e, heI, hins⟩ := exists_insert_of_not_maximal indep_subset hI hImax

Goal state after:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
⊢ ∃ x ∈ B \ I, Indep (insert x I)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
⊢ a * (toAlgebra e) m = e (a ⊗ₜ[R] m)

Tactic:
dsimp [toAlgebra]

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
⊢ a * e ((algebraMap R A) 1 ⊗ₜ[R] m) = e (a ⊗ₜ[R] m)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ insert e (⋃ i, I i) ⊆ M.E

Tactic:
rw [insert_subset_iff, iUnion_subset_iff, and_iff_left (fun i ↦ (hI i).indep.subset_ground)]

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ e ∈ M.E