mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case refine_2
R : Type u
S : Type v
ι : Type w
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
P✝ : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
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 ι
x : ↥Q.ker
⊢ ((↑x).coeff.sum fun n r ↦ (rename Sum.inr) (P.σ r) * (monomial (Finsupp.mapDomain Sum.inl n)) 1) ∈ (Q.comp P).ker

Tactic:
· simp only [ker_eq_ker_aeval_val, RingHom.mem_ker]
    conv_rhs => rw [← aeval_val_eq_zero x.2, ← x.1.support_sum_monomial_coeff]
    simp only [Finsupp.sum, map_sum, map_mul, aeval_rename, Function.comp_def, comp_val,
      Sum.elim_inr, aeval_monomial, map_one, Finsupp.prod_mapDomain_index_inj Sum.inl_injective,
      Sum.elim_inl, one_mul]
    congr! with v i
    simp_rw [← IsScalarTower.toAlgHom_apply R, ← comp_aeval, AlgHom.comp_apply, P.aeval_val_σ,
      coeff]

Goal state after:
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
⊢ IsTrivialRelation f x

Tactic:
have : x' f' = 0 := by simpa [x', f', linearCombination_apply, sum_fintype] using hfx

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
this : x' f' = 0
⊢ IsTrivialRelation f x
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ p ∈ support R M → ∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal

Tactic:
contrapose
    rw [notMem_support_iff, LocalizedModule.subsingleton_iff_ker_eq_top, ← top_le_iff,
      ← hs, Submodule.span_le, Set.subset_def]
    simp_rw [SetLike.le_def, Submodule.mem_annihilator_span_singleton, SetLike.mem_coe,
      LocalizedModule.mem_ker_mkLinearMap_iff]
    push Not
    simp_rw [and_comm]
    exact id

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
⊢ support R N = support R M ∪ support R P

Tactic:
refine subset_antisymm ?_ (Set.union_subset (Module.support_subset_of_injective f hf)
    (Module.support_subset_of_surjective g hg))
  intro x
  contrapose
  simp only [Set.mem_union, not_or, and_imp, notMem_support_iff']
  intro H₁ H₂ m
  obtain ⟨r, hr, e₁⟩ := H₂ (g m)
  rw [← map_smul, h] at e₁
  obtain ⟨m', hm'⟩ := e₁
  obtain ⟨s, hs, e₁⟩ := H₁ m'
  exact ⟨_, x.asIdeal.primeCompl.mul_mem hs hr, by rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type w
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
t : Set R
ht : Ideal.span t = ⊤
Mₚ : ↑t → Type u_1
inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)
inst✝⁴ : (g : ↑t) → Module R (Mₚ g)
Rₚ : ↑t → Type u_2
inst✝³ : (g : ↑t) → CommSemiring (Rₚ g)
inst✝² : (g : ↑t) → Algebra R (Rₚ g)
h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)
inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)
inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↑t) → M →ₗ[R] Mₚ g
h₂ : ∀ (g : ↑t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↑t), Module.Finite (Rₚ g) (Mₚ g)
⊢ Module.Finite R M

Tactic:
Ideal.span_eq_top_iff_finite

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
M : Type w
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
t : Set R
ht : ∃ s', ↑s' ⊆ t ∧ Ideal.span ↑s' = ⊤
Mₚ : ↑t → Type u_1
inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)
inst✝⁴ : (g : ↑t) → Module R (Mₚ g)
Rₚ : ↑t → Type u_2
inst✝³ : (g : ↑t) → CommSemiring (Rₚ g)
inst✝² : (g : ↑t) → Algebra R (Rₚ g)
h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)
inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)
inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↑t) → M →ₗ[R] Mₚ g
h₂ : ∀ (g : ↑t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↑t), Module.Finite (Rₚ g) (Mₚ g)
⊢ Module.Finite R M
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
⊢ (LinearMap.rTensor N₂ f₂ ∘ₗ LinearMap.lTensor M₂ g₁) x = (LinearMap.lTensor M₃ g₁ ∘ₗ LinearMap.rTensor N₁ f₂) x

Tactic:
LinearMap.rTensor_comp_lTensor,

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
⊢ (map f₂ g₁) x = (LinearMap.lTensor M₃ g₁ ∘ₗ LinearMap.rTensor N₁ f₂) x
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0
y : M₁ ⊗[R] N₂
hy : (LinearMap.rTensor N₂ f₁) y = (LinearMap.lTensor M₂ g₁) x
⊢ (LinearMap.rTensor N₃ f₁ ∘ₗ LinearMap.lTensor M₁ g₂) y = (LinearMap.lTensor M₂ g₂ ∘ₗ LinearMap.rTensor N₂ f₁) y

Tactic:
LinearMap.rTensor_comp_lTensor,

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
this : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0
y : M₁ ⊗[R] N₂
hy : (LinearMap.rTensor N₂ f₁) y = (LinearMap.lTensor M₂ g₁) x
⊢ (map f₁ g₂) y = (LinearMap.lTensor M₂ g₂ ∘ₗ LinearMap.rTensor N₂ f₁) y
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
inst : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
⊢ (FreeAddMonoid.lift φ) (FreeAddMonoid.of (z, update f i m₁) + FreeAddMonoid.of (z, update f i m₂)) =
    (FreeAddMonoid.lift φ) (FreeAddMonoid.of (z, update f i (m₁ + m₂)))

Tactic:
by simp [FreeAddMonoid.lift_eval_of, @C_add inst]

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 = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹

Tactic:
← hj.mul_left_inj,

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 j = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹ * a n j
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
r : R
⊢ algebraMap₀ r = r • GradedMonoid.GOne.one

Tactic:
simp [algebraMap₀]; congr

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
⊢ reindex R s e ≪≫ₗ reindex R (fun i ↦ s (e.symm i)) e' = reindex R s (e.trans e')

Tactic:
apply LinearEquiv.toLinearMap_injective
  ext f
  simp only [LinearEquiv.trans_apply, LinearEquiv.coe_coe, reindex_tprod,
    LinearMap.coe_compMultilinearMap, Function.comp_apply,
    reindex_comp_tprod]
  congr

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
⊢ LinearIndependent R ![↑a, ↑b]

Tactic:
have := h.comp ![a, b] fun i j hij ↦ by
    fin_cases i <;> fin_cases j
    · rfl
    · simp [hab] at hij
    · simp [hab.symm] at hij
    · rfl

Goal state after:
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])
⊢ LinearIndependent R ![↑a, ↑b]
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
hp : finrank R (M × N) = n + 1
⊢ finrank R ↥(⋀[R]^(n + 1) (M × N)) = 1

Tactic:
by simp [exteriorPower.finrank_eq, hp]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Finite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
inst✝¹ : Module.Finite A B
x : B
inst✝ : Module.Free A B
⊢ (minpoly A x).natDegree ≤ Module.finrank A B

Tactic:
by
  nontriviality A
  simpa [Module.finrank_eq_spanFinrank_of_free] using natDegree_le_spanFinrank A x

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
⊢ IsSolvable ↥⊤

Tactic:
induction (⊤ : Subgroup G) using WellFoundedLT.induction with | ind H hH

Goal state after:
case ind
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
⊢ IsSolvable ↥H
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero.refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b ∈ ⊥

Tactic:
rw [← hn]
          exact mem_top _

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ ⊥

Tactic:
rw [← hn]
          exact mem_top _

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
p : PrimeSpectrum R
⊢ rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)

Tactic:
by
  let e : LocalizedModule p.asIdeal.primeCompl M ≃ₗ[Localization.AtPrime p.asIdeal]
      Localization.AtPrime p.asIdeal ⊗[R] M :=
    LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M
  rw [rankAtStalk, e.finrank_eq]

Goal state after:
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
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
⊢ (⨆ f, f.fieldRange).val x ∈ ↑(IntermediateField.map (⨆ f, f.fieldRange).val (⨆ f, f.fieldRange))

Tactic:
IntermediateField.map_iSup

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
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
⊢ (⨆ f, f.fieldRange).val x ∈ ↑(⨆ i, IntermediateField.map (⨆ f, f.fieldRange).val i.fieldRange)
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := ⋯
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := ⋯
β_in_Fγ : β ∈ F⟮γ⟯
⊢ F⟮γ⟯ ≤ F⟮α, β⟯

Tactic:
adjoin_simple_le_iff

Goal state after:
case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ γ ∈ F⟮α, β⟯
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K K' : IntermediateField F L
inst✝ : Normal F L
h : K ≤ K'
⊢ normalClosure F (↥K) L ≤ normalClosure F (↥K') L

Tactic:
by
  rw [normalClosure_def', normalClosure_def']
  exact iSup_mono (fun f ↦ map_mono f h)

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α + x • β⟯ ≤ F⟮α, β⟯

Tactic:
adjoin_simple_le_iff

Goal state after:
case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ α + x • β ∈ F⟮α, β⟯
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
rw [h, encard_empty, encard_eq_zero, eq_empty_iff_forall_notMem] at hcard

Goal state after:
case inl
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : ∀ (x : α), x ∉ B' \ B
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))
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'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))

Tactic:
refine ⟨f, hf, by_contra fun hnot ↦ ?_⟩

Goal state after:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
by
  obtain ⟨B', hB', hIB'⟩ := hI.exists_isBase_superset
  obtain ⟨x, hxB', hx⟩ := exists_of_ssubset (hIB'.ssubset_of_ne (by (rintro rfl; exact hI' hB')))
  by_cases hxB : x ∈ B
  · exact ⟨x, ⟨hxB, hx⟩, hB'.indep.subset (insert_subset hxB' hIB')⟩
  obtain ⟨e, he, hBase⟩ := hB'.exchange hB ⟨hxB', hxB⟩
  exact ⟨e, ⟨he.1, notMem_subset hIB' he.2⟩,
    indep_iff.2 ⟨_, hBase, insert_subset_insert (subset_sdiff_singleton hIB' hx)⟩⟩

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

Goal state before:
pp: α : Type u_1
E I X : Set α
⊢ I = ∅ ∧ X ⊆ E → (loopyOn E).IsBasis I X

Tactic:
rintro ⟨rfl, hX⟩

Goal state after:
α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).IsBasis ∅ X
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ B = I ∩ E

Tactic:
rw [h, inter_comm I]

Goal state after:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ (E \ I) = E ∩ I
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K ↦ P K ∧ K ⊆ X) J

Tactic:
have hfin : Set.Finite (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}) := by
    rw [finite_iff_bddAbove, bddAbove_def]
    simp_rw [ENat.le_natCast_iff] at hP
    use n
    rintro x ⟨Y, ⟨hY, -, -⟩, rfl⟩
    obtain ⟨n₀, heq, hle⟩ := hP Y hY
    rwa [ncard_def, heq, ENat.toNat_natCast]

Goal state after:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K ↦ P K ∧ K ⊆ X) J