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

Goal state before:
pp: case insert.specialize_2.e_a.e_a.e_a
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)
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
hfv : ∑ x ∈ s, f x • v x + ((-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹) • v n✝ = 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⁻¹
⊢ (∑ x ∈ s, f x * if x = ↑n then 0 else a' x) = ∑ i ∈ s, f i * a' i

Tactic:
exact s.sum_congr rfl fun i hi ↦ by rw [if_neg (ne_of_mem_of_not_mem hi hn)]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Bijective
    ⇑((IsLocalizedModule.map P.primeCompl (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization P.primeCompl)))
          ((TensorProduct.mk R (Localization P.primeCompl) M) 1))
        (Finsupp.linearCombination R b))

Tactic:
IsLocalizedModule.map_linearCombination,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : Fin n → M
hb : ∀ (i : Fin n), (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ i.asIdeal) M) 1) (b i) = fun x ↦ (b' x) i
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Bijective
    ⇑(↑R
        (Finsupp.linearCombination (Localization P.primeCompl)
          (⇑((TensorProduct.mk R (Localization P.primeCompl) M) 1) ∘ b)))
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝¹ : CommRing A
inst✝ : IsNoetherianRing A
I : Ideal A
h : Disjoint ↑I ↑(nonZeroDivisors A)
x : A
hP : I ≤ ⊥.colon {x}
prime : (⊥.colon {x}).IsPrime
⊢ ∀ n ∈ I, x • n = 0

Tactic:
by
    simpa only [smul_eq_mul, mul_comm x, SetLike.le_def, Submodule.mem_colon_singleton] using! hP

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

Goal state before:
pp: case mp
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
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J) → ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J

pp: case mpr
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
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J) → ∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J

Tactic:
· rintro ⟨X, ⟨x, hX⟩, hx⟩
    refine ⟨x, ?_, ?_⟩
    · rintro rfl; simp [X.ne_zero.symm] at hX
    simpa only [hX, mul_comm] using! hx

Goal state after:
case mpr
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
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J) → ∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
x✝ : Free R M
a✝ : Nontrivial R
⊢ Nonempty (M ≃ₗ[R] R)

Tactic:
have e := (Free.chooseBasis R M).repr

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
x✝ : Free R M
a✝ : Nontrivial R
e : M ≃ₗ[R] Free.ChooseBasisIndex R M →₀ R
⊢ Nonempty (M ≃ₗ[R] R)
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set ι
H : AlgebraicIndepOn R x t
hst : s ⊆ t
⊢ AlgebraicIndepOn R x s

Tactic:
simpa [Function.comp] using! H.comp (Set.inclusion hst) (Set.inclusion_injective hst)

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: 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)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
x : ↥↑I
⊢ ↑(∑ d, f x d • ⟨b d, ⋯⟩) = ↑(LinearMap.id x)

Tactic:
coe_sum,

Goal state after:
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)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
x : ↥↑I
⊢ ∑ i, ↑(f x i • ⟨b i, ⋯⟩) = ↑(LinearMap.id x)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔
    (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y

Tactic:
refine ⟨fun h ↦ ⟨⟨_, h, disjoint_sdiff_right⟩,
    fun I hI B' ⟨hB', hIB'⟩ hBI ↦ hBI.antisymm ?_⟩, fun ⟨⟨B', hB', hBB'⟩,h⟩ ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ I ⊆ B

case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
⊢ M.IsBase (M.E \ B)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ ∃ J, M.IsBasis J Y ∧ J ∩ X = I

Tactic:
by
  obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans hXY)
  refine ⟨J, hJ, subset_antisymm ?_ (subset_inter hIJ hI.subset)⟩
  exact fun e he ↦ hI.mem_of_insert_indep he.2 (hJ.indep.subset (insert_subset he.1 hIJ))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
R✝ I X Y : Set α
inst✝ : M.Finitary
R : Set α
⊢ (M ↾ R).Finitary

Tactic:
refine ⟨fun I hI ↦ ?_⟩

Goal state after:
α : Type u_1
M : Matroid α
R✝ I✝ X Y : Set α
inst✝ : M.Finitary
R I : Set α
hI : ∀ J ⊆ I, J.Finite → (M ↾ R).Indep J
⊢ (M ↾ R).Indep I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N✝ N : Matroid β
inst✝ : N.Finitary
f : α → β
⊢ (N.comap f).Finitary

Tactic:
refine ⟨fun I hI ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
⊢ (N.comap f).Indep I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) (insert e C)

Tactic:
← insert_sdiff_singleton,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) (insert e (C \ {e}))
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Finitary

Tactic:
refine ⟨fun I hI ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
⊢ (M.map f hf).Indep I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
h' : I ⊆ f '' M.E
⊢ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
obtain ⟨I₀, hI₀E, rfl⟩ := subset_image_iff.1 h'

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I₀ : Set α
hI₀E : I₀ ⊆ M.E
hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J
h' : f '' I₀ ⊆ f '' M.E
⊢ ∃ I₀_1, M.Indep I₀_1 ∧ f '' I₀ = f '' I₀_1
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
I : Set α
e : α
M : Matroid α
aux : ∀ (A B : Set α), M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B
⊢ (M ↾ univ).fundCircuit e I = M.fundCircuit e I

Tactic:
simp [fundCircuit, aux]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
⊢ M.eRk (insert e I) = I.encard + 1

Tactic:
Indep.eRk_eq_encard (by tauto),

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
⊢ (insert e I).encard = I.encard + 1
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ X ⊆ M.closure X

Tactic:
by
  simp [M.closure_def' X, subset_sInter_iff]

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ M.fundCircuit x B \ {x} ⊆ B

Tactic:
simpa using fundCircuit_subset_insert ..

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
⊢ (∀ ⦃B : Set α⦄, (M ↾ X).IsBase B → #↑B ≤ κ) ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #↑I ≤ κ

Tactic:
isBase_restrict_iff'

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

Goal state before:
pp: case inl
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)

Tactic:
rw [h _ (sdiff_subset.trans hI)]

Goal state after:
case inl
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
⊢ Disjoint (I \ M₁.coloops) (M₁.loops ∪ M₁.coloops)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case neg
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : ¬M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Tactic:
simp [hI, show ¬ M.Indep (insert e I) from fun h ↦ hI <| h.subset <| subset_insert _ _]

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

Goal state before:
pp: case pos
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ M✶.fundCircuit e (M✶.E \ X) = {e}

Tactic:
fundCircuit_eq_of_mem

Goal state after:
case pos
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ {e} = {e}

case pos
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ e ∈ M✶.E \ X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ M.closure (⋂ i, Is i) = ⋂ i, M.closure (Is i)

Tactic:
convert!
    h.closure_sInter_eq_biInter_closure_of_forall_subset (range_nonempty Is)
      (by simp [subset_iUnion])

Goal state after:
case e'_3
α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ ⋂ i, M.closure (Is i) = ⋂ J ∈ range Is, M.closure J
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : ¬Injective ⇑(algebraMap R A)
⊢ trdeg R A = 0

Tactic:
have := isEmpty_algebraicIndependent h

Goal state after:
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : ¬Injective ⇑(algebraMap R A)
this : IsEmpty { s // AlgebraicIndepOn R _root_.id s }
⊢ trdeg R A = 0
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ ¬M.closure S = M.E → M.closure S ⊆ M.E

Tactic:
iff_true_intro (M.closure_subset_ground _)

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ ¬M.closure S = M.E → True
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
⊢ M.closure I = M.E ↔ M.closure X = M.E

Tactic:
hIX.closure_eq_closure

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
⊢ M.closure X = M.E ↔ M.closure X = M.E
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
⊢ orbit (↥(fixingSubgroup M sᶜ)) a ⊆ s

Tactic:
by
  intro b b_in_orbit
  let ⟨⟨g, g_fixing⟩, g_eq⟩ := MulAction.mem_orbit_iff.mp b_in_orbit
  rw [Submonoid.mk_smul] at g_eq
  rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing
  rwa [← g_eq, smul_mem_of_set_mem_fixedBy (set_mem_fixedBy_of_movedBy_subset g_fixing)]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
⊢ ((AlgebraicIndepOn R _root_.id s ∧ s ⊆ t) ∧ ∀ x ∉ s, ¬(AlgebraicIndepOn R _root_.id (insert x s) ∧ insert x s ⊆ t)) ∧
      t ⊆ (matroid R A).E ↔
    (AlgebraicIndepOn R _root_.id s ∧ s ⊆ t) ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a

Tactic:
matroid_e,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
⊢ ((AlgebraicIndepOn R _root_.id s ∧ s ⊆ t) ∧ ∀ x ∉ s, ¬(AlgebraicIndepOn R _root_.id (insert x s) ∧ insert x s ⊆ t)) ∧
      t ⊆ univ ↔
    (AlgebraicIndepOn R _root_.id s ∧ s ⊆ t) ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ Maximal (fun A_1 ↦ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t

Tactic:
matroid_e,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ Maximal (fun A_1 ↦ A_1 ⊆ t) s ∧ t ⊆ univ ↔ s = t
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A

Tactic:
matroid_e,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ (matroid R A).closure s = univ ∧ s ⊆ univ ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ (∀ ⦃I X : Set A⦄, (matroid R A).IsBasis I s → (matroid R A).IsBasis I X → X ⊆ s) ∧ s ⊆ (matroid R A).E

Tactic:
matroid_e,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ (∀ ⦃I X : Set A⦄, (matroid R A).IsBasis I s → (matroid R A).IsBasis I X → X ⊆ s) ∧ s ⊆ univ
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ ⋂₀ {F | s ∩ (matroid R A).E ⊆ F} = s

Tactic:
matroid_e,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ ⋂₀ {F | s ∩ univ ⊆ F} = s
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ s = univ

Tactic:
matroid_e,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ s = univ ∧ s ⊆ univ ↔ s = univ
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
A : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this : NoZeroDivisors S
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)

Tactic:
have := (FaithfulSMul.algebraMap_injective R S).nontrivial

Goal state after:
R : Type u_1
S : Type v
A : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
have := H₂.nontrivial

Goal state after:
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∈ s
⊢ v j ∈ (matroid R S).closure (v '' s \ {v j})

Tactic:
by
    rw [← image_singleton, ← inj.image_sdiff_subset (singleton_subset_iff.mpr hj)]
    rwa [insert_eq_of_mem hi] at H₂

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg.refine_2.inl
F : Type u
inst✝ : Field F
h : ¬0 = 0 ∧ ¬0 = 0
⊢ ∀ (a : AlgebraicClosure F), 0 ≠ 0 ∧ (aeval a) 0 = 0 → ∀ (b : AlgebraicClosure F), 0 ≠ 0 ∧ (aeval b) 0 = 0 → a ≠ b

Tactic:
exact (h.1 rfl).elim

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)

Tactic:
· intro x₀
    rw [basis.tendsto_iff basis]
    intro U U_in
    exact conj x₀ U_in

Goal state after:
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
| finrank (↥K) E

Tactic:
← fixedField_fixingSubgroup K,

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
| finrank (↥(fixedField K.fixingSubgroup)) E