mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ (-1) ^ ↑i • (f (v j)) (i.removeNth v) + (-1) ^ ↑j • (f (v j)) (j.removeNth v) = 0

Tactic:
neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ 0 = 0

case hvij
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ v i = v j

case hij
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ i ≠ j
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
this : N₂ ≤ 𝔪 • N₂ ⊔ N₁
⊢ N₁ = N₂

Tactic:
rw [sup_comm] at this

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ 𝔪 • N₂
⊢ N₁ = N₂
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ ((Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s)) s = 1

Tactic:
simpa [basis_repr_apply] using ιMultiDual_apply_diag R n b s

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: case inl
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
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h✝ : Flat R ↥M
⊢ LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)

pp: case inr
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
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h✝ : Flat R ↥N
⊢ LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
· exact H.linearIndependent_mul_of_flat_left hm hn

Goal state after:
case inr
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
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h✝ : Flat R ↥N
⊢ LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)
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 := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : map (Submodule.subtype K) (span R ↑s) = K
z : R := ∏ y ∈ s, f y
hz : z ∉ I
⊢ ↑s ⊆ ⇑(Submodule.subtype K) ⁻¹' ↑(N.colon {z • x})

Tactic:
intro i

Goal state after:
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 := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : map (Submodule.subtype K) (span R ↑s) = K
z : R := ∏ y ∈ s, f y
hz : z ∉ I
i : ↥K
⊢ i ∈ ↑s → i ∈ ⇑(Submodule.subtype K) ⁻¹' ↑(N.colon {z • x})
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case insert.inl
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 : ∀ 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
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⁻¹
hi : i = n✝
⊢ ∀ x ∈ s, f x * a' x = 0

Tactic:
intro i

Goal state after:
case insert.inl
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 : ∀ 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
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⁻¹
hi : i✝ = n✝
i : ι
⊢ i ∈ s → f i * a' 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 := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K ≤ N.colon {z • x}
⊢ ∀ z_1 ∈ K, z * z_1 ∈ ann

Tactic:
intro i

Goal state after:
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 := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K ≤ N.colon {z • x}
i : R
⊢ i ∈ K → z * i ∈ ann
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case e_6
R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑((Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv)
        ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)) =
    ↑((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)

Tactic:
Units.coe_mapEquiv,

Goal state after:
case e_6
R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv ↑((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    ↑((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case e_6
R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv ↑((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    ↑((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)

Tactic:
Units.coe_mapEquiv,

Goal state after:
case e_6
R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv ↑((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    ↑(canonicalEquiv R⁰ K K') ↑I
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: 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
⊢ ∃ g, f ∘ₗ g = id

Tactic:
change LinearMap.id ∈ LinearMap.range (LinearMap.llcomp R N M N f)
  refine Submodule.mem_of_localization_maximal _ (fun P _ ↦ LocalizedModule.map P.primeCompl) _ _
    fun I hI ↦ ?_
  rw [LocalizedModule.map_id]
  have : LinearMap.id ∈ LinearMap.range (LinearMap.llcomp _
    (LocalizedModule I.primeCompl N) _ _ (LocalizedModule.map I.primeCompl f)) := H I hI
  convert! this
  · ext f
    constructor
    · intro hf
      obtain ⟨a, ha, c, rfl⟩ := hf
      obtain ⟨g, rfl⟩ := ha
      use IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g c
      apply ((Module.End.isUnit_iff _).mp <| IsLocalizedModule.map_units
        (LocalizedModule.map I.primeCompl) c).injective
      dsimp
      conv_rhs => rw [← Submonoid.smul_def]
      conv_lhs => rw [← LinearMap.map_smul_of_tower]
      rw [← Submonoid.smul_def, IsLocalizedModule.mk'_cancel', IsLocalizedModule.mk'_cancel']
      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 [LocalizedModule.map_mk, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
        Function.comp_apply, LocalizedModule.mkLinearMap_apply, LinearMap.llcomp_apply,
        LocalizedModule.map_mk]
    · 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.RingTheory.Localization.Free

Goal state before:
pp: case refine_2
R : Type u_4
M : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
f : M →ₗ[R] M'
inst✝⁷ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁶ : CommRing Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : IsScalarTower R Rₛ M'
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
this : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)
he :
  LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ ∘ₗ ↑R ↑e =
    ↑(LinearEquiv.restrictScalars R b.repr) ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] I →₀ Localization (Submonoid.powers r) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
⊢ ∀ (i : I),
    (LocalizedModule.lift (Submonoid.powers r) f ⋯)
        ({
            repr :=
              e ≪≫ₗ
                let __spread.0 := e';
                let __LinearMap :=
                  ↑(LinearEquiv.extendScalarsOfIsLocalization (Submonoid.powers r) (Localization (Submonoid.powers r))
                      e');
                { toLinearMap := __LinearMap, invFun := __spread.0.invFun, left_inv := ⋯, right_inv := ⋯ } }
          i) =
      b i

Tactic:
intro i

Goal state after:
case refine_2
R : Type u_4
M : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
f : M →ₗ[R] M'
inst✝⁷ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁶ : CommRing Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : IsScalarTower R Rₛ M'
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
this : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)
he :
  LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ ∘ₗ ↑R ↑e =
    ↑(LinearEquiv.restrictScalars R b.repr) ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] I →₀ Localization (Submonoid.powers r) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
i : I
⊢ (LocalizedModule.lift (Submonoid.powers r) f ⋯)
      ({
          repr :=
            e ≪≫ₗ
              let __spread.0 := e';
              let __LinearMap :=
                ↑(LinearEquiv.extendScalarsOfIsLocalization (Submonoid.powers r) (Localization (Submonoid.powers r))
                    e');
              { toLinearMap := __LinearMap, invFun := __spread.0.invFun, left_inv := ⋯, right_inv := ⋯ } }
        i) =
    b i
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)
this : (i : ι) → Module (Localization S) (M' i) := ⋯
⊢ ∀ (i : ι), IsBaseChange (Localization S) (f i)

Tactic:
intro i

Goal state after:
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)
this : (i : ι) → Module (Localization S) (M' i) := fun i ↦ module S (f i)
i : ι
⊢ IsBaseChange (Localization S) (f i)
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Subsingleton G
⊢ ⊤ = ⊥

Tactic:
simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝² : Group G
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ IsSolvable G

Tactic:
obtain ⟨m, hm⟩ := id hG'

Goal state after:
G : Type u_1
inst✝² : Group G
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ IsSolvable G
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ x = ↑α ^ n

Tactic:
norm_cast

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ x = ↑(α ^ n)
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
⊢ ∀ (i : ι), (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x)).Splits

Tactic:
intro i

Goal state after:
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
i : ι
⊢ (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x)).Splits
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ B ⊂ insert x (insert f (B \ {x}))

Tactic:
rw [insert_comm, insert_sdiff_singleton, insert_eq_of_mem he.1]

Goal state after:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ B ⊂ insert f B
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
IF : Type (max 0 u_2) := { K // ∃ x, K = F⟮x⟯ }
this✝ : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional F ↥↑K
hfin : FiniteDimensional F ↥(⨆ i, ↑i)
⊢ FiniteDimensional F E

Tactic:
have htop : ⨆ K : IF, K.1 = ⊤ := le_top.antisymm fun x _ ↦
    le_iSup (fun K : IF ↦ K.1) ⟨F⟮x⟯, x, rfl⟩ <| mem_adjoin_simple_self F x

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
IF : Type (max 0 u_2) := { K // ∃ x, K = F⟮x⟯ }
this✝ : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional F ↥↑K
hfin : FiniteDimensional F ↥(⨆ i, ↑i)
htop : ⨆ K, ↑K = ⊤
⊢ FiniteDimensional F E
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E

Tactic:
IsBasis,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
⊢ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E ↔
    (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X) I ↔ M.IsBasis I (X ∩ M.E)

Tactic:
IsBasis,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
⊢ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X) I ↔ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X ∩ M.E) I ∧ X ∩ M.E ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ M.IsBasis I X ↔ Maximal (fun I ↦ M.Indep I ∧ I ⊆ X) I

Tactic:
IsBasis,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E ↔ Maximal (fun I ↦ M.Indep I ∧ I ⊆ X) I
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBasis B M.E ↔ M.IsBase B

Tactic:
IsBasis,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
⊢ Maximal (fun A ↦ M.Indep A ∧ A ⊆ M.E) B ∧ M.E ⊆ M.E ↔ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ M.IsBasis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I)

Tactic:
IsBasis,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E ↔ ∀ e ∈ X \ I, M.Dep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
⊢ I ≠ B''ᶜ ∩ M.E

Tactic:
by { rintro rfl; apply hI; convert! hB''; simp [hB''.subset_ground] }

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ M.IsBasis (I ∪ I' \ I) Y

Tactic:
rwa [union_sdiff_self, union_eq_self_of_subset_left hII']

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ Maximal (M ↾ X).Indep I ↔ M.IsBasis I X

Tactic:
IsBasis,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ Maximal (M ↾ X).Indep I ↔ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I X → I ⊆ R

Tactic:
exact fun h ↦ h.subset.trans hXR

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ M ↾ N.E = N

Tactic:
by
  obtain ⟨R, -, rfl⟩ := h; rw [restrict_ground_eq]

Goal state after: