mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
E : Set α
M N : Matroid α
hM : M.E = E
hN : N.E = E
h : M.restrictSubtype E = N.restrictSubtype E
⊢ M = N

Tactic:
by
  subst hM
  refine ext_indep (by rw [hN]) (fun I hI ↦ ?_)
  rwa [← restrictSubtype_indep_iff_of_subset hI, h, restrictSubtype_indep_iff_of_subset]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.IsNonloop e ↔ e ∈ M.E \ M.loops

Tactic:
rw [isNonloop_iff, IsLoop, and_comm, mem_sdiff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
h : I = ∅
⊢ X ∩ M.E ⊆ M.loops

Tactic:
by simpa [h] using! hI

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

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
⊢ M.RankInfinite

Tactic:
by assumption

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

Goal state before:
pp: case refine_5
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ range x, M.IsCircuit C' ∧ z ∈ C'

Tactic:
obtain ⟨C', hC'ss, hC', hzC'⟩ := hwin
    refine ⟨C', hC'ss.trans ?_, hC', hzC'⟩
    refine union_subset (sdiff_subset_sdiff_left subset_union_left)
      (iUnion_subset fun i ↦ subset_sdiff.2
        ⟨sdiff_subset.trans (subset_union_of_subset_right (subset_iUnion ..) _), ?_⟩)
    rw [disjoint_iff_forall_ne]
    rintro _ he _ ⟨j, hj, rfl⟩ rfl
    obtain rfl : j = i := h_unique he.1
    simp at he

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

Goal state before:
pp: α : Type u_1
X Y : Set α
hXY : X ⊆ Y
⊢ (freeOn Y).eRk X = X.encard

Tactic:
obtain ⟨I, hI⟩ := (freeOn Y).exists_isBasis X

Goal state after:
α : Type u_1
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : (freeOn Y).IsBasis I X
⊢ (freeOn Y).eRk X = X.encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ (B ∩ X).encard + (M.E \ B).encard = (M.E \ B ∩ (M.E \ X)).encard + X.encard

Tactic:
← encard_union_eq (by tauto_set),

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ (B ∩ X ∪ M.E \ B).encard = (M.E \ B ∩ (M.E \ X)).encard + X.encard
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
⊢ #↑I ≤ M.cRk Y

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hIX.indep.subset_isBasis'_of_subset (hIX.subset.trans hXY)

Goal state after:
α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ #↑I ≤ M.cRk Y
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M N : Matroid α
hNM : N ≤r M
inst✝ : N.Loopless
⊢ N ≤r M.removeLoops

Tactic:
by
  obtain ⟨R, hR, rfl⟩ := hNM.exists_eq_restrict
  exact IsRestriction.of_subset M fun e heR ↦ ((M ↾ R).isNonloop_of_loopless heR).of_restrict

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ Disjoint C K ∨ (C ∩ K).Nontrivial

Tactic:
by
  rw [or_iff_not_imp_left, disjoint_iff_inter_eq_empty, ← ne_eq, ← nonempty_iff_ne_empty]
  exact hC.isCocircuit_inter_nontrivial hK

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

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M✶.RankPos
⊢ M✶.RankPos

Tactic:
by assumption

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I J : Set α
hI : M.IsBasis I X
hJI : J ⊆ I
hJ : X ⊆ M.closure J
⊢ J = I

Tactic:
rw [← hI.indep.closure_inter_eq_self_of_subset hJI, inter_eq_self_of_subset_right]

Goal state after:
α : Type u_2
M : Matroid α
X I J : Set α
hI : M.IsBasis I X
hJI : J ⊆ I
hJ : X ⊆ M.closure J
⊢ I ⊆ M.closure J
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case refine_2.inr
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
heJI : e ∈ J \ I
⊢ e ∈ M.closure (I ∪ J \ {e})

Tactic:
← sdiff_singleton_eq_self heJI.2,

Goal state after:
case refine_2.inr
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
heJI : e ∈ J \ I
⊢ e ∈ M.closure (I \ {e} ∪ J \ {e})
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case e'_1
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ AlgebraicIndependent R (Sum.elim (fun i ↦ x ↑i) fun i ↦ x ↑i) ↔ AlgebraicIndependent R x

Tactic:
apply algebraicIndependent_equiv' ((Equiv.sumComm ..).trans (Equiv.Set.sumCompl ..))

Goal state after:
case e'_1
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ x ∘ ⇑((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)) = Sum.elim (fun i ↦ x ↑i) fun i ↦ x ↑i
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
S : Type u
A : Type v
x : ι → A
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
hx : AlgebraicIndependent R x
ι' : Type u_4
y : ι' → A
hxS : range x ⊆ range ⇑(algebraMap S A)
hy : AlgebraicIndependent S y
e : S ≃ₐ[R] ↥(IsScalarTower.toAlgHom R S A).range := AlgEquiv.ofInjective (IsScalarTower.toAlgHom R S A) ⋯
Rx : Subalgebra R A := adjoin R (range x)
x✝ : Algebra (↥Rx) S := ((↑e.symm).comp (Subalgebra.inclusion ⋯)).toAlgebra
this : IsScalarTower (↥Rx) S A
⊢ Injective ⇑↑(Subalgebra.inclusion ⋯)

Tactic:
simpa only [AlgHom.coe_toRingHom] using Subalgebra.inclusion_injective _

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

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : M.Spanning S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
by
  rwa [spanning_iff_exists_isBase_subset] at hS

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand : (expand F (q ^ m)) g = (expand F (q ^ m * q ^ s)) g'
hm : m ≤ m + s
⊢ g.natDegree = g'.natDegree

Tactic:
expand_mul,

Goal state after:
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand : (expand F (q ^ m)) g = (expand F (q ^ m)) ((expand F (q ^ s)) g')
hm : m ≤ m + s
⊢ g.natDegree = g'.natDegree
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m)) g = f
g' : F[X] := Classical.choose hf
hg' : (Classical.choose hf).Separable
m' : ℕ
hm' : (expand F (q ^ m')) (Classical.choose hf) = f
⊢ Nat.Prime q

Tactic:
by assumption

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

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]

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

Goal state before:
pp: case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
p : Surjective fun i ↦ ⟨x i, ⋯⟩
q : (Subtype.val '' range fun i ↦ ⟨x i, ⋯⟩) = Subtype.val '' univ
⊢ range x = w

Tactic:
rw [← image_univ, image_image] at q

Goal state after:
case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
p : Surjective fun i ↦ ⟨x i, ⋯⟩
q : (fun x_1 ↦ ↑⟨x x_1, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range x = w
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
n : ℕ
⊢ (X ^ n).natSepDegree = if n = 0 then 0 else 1

Tactic:
simp only [natSepDegree_pow, natSepDegree_X]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x✝ : ∃ x, C x = g
x : F
h : C x = g
⊢ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g

Tactic:
by_cases hx : x = 0
      · exact .inl ⟨rfl, by rw [← h, hx, map_zero]⟩
      exact .inr ⟨x, Ne.isUnit hx, h⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this : FiniteDimensional F ↥E'
g : (↥E')[X] := f.toSubring E'.toSubring ⋯
h : Polynomial.map (algebraMap (↥E') E) g = f
⊢ IsSeparable F x

Tactic:
clear_value g

Goal state after:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
⊢ IsSeparable F x
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field E'
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F E'
inst✝³ : Algebra E E'
inst✝² : IsScalarTower F E E'
L : IntermediateField F E
inst✝¹ : Normal F E
inst✝ : Normal F E'
⊢ (map (IsScalarTower.toAlgHom F E E') L).fixingSubgroup.index = L.fixingSubgroup.index

Tactic:
rw [L.map_fixingSubgroup E', L.fixingSubgroup.index_comap_of_surjective
    (AlgEquiv.restrictNormalHom_surjective _)]

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
⊢ IsCyclic Gal(K/F)

Tactic:
have := finrank_eq_two F K ▸ AlgEquiv.card_le
  rw [← Nat.card_eq_fintype_card] at this
  interval_cases h : Nat.card Gal(K/F)
  · simp_all
  · exact @isCyclic_of_subsingleton _ _ (Finite.card_le_one_iff_subsingleton.mp h.le)
  · exact isCyclic_of_prime_card h

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
⊢ ∃ z, z ^ n = x

Tactic:
have hn' : 0 < n := Nat.pos_of_ne_zero fun h => by
    rw [h, Nat.cast_zero] at hn
    exact hn.out rfl

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
⊢ ∃ z, z ^ n = x
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case hcard
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ (∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r).natDegree <
    Fintype.card (L →ₐ[K] E)

Tactic:
refine (Polynomial.natDegree_sub_le _ _).trans_lt
      (max_lt ((Polynomial.natDegree_sum_le _ _).trans_lt ?_) ?_)
    · simp only [Polynomial.map_smul,
        map_div₀, map_pow, RingHom.coe_coe, Function.comp_apply,
        Finset.mem_univ, forall_true_left, Finset.fold_max_lt, AlgHom.card]
      refine ⟨finrank_pos, ?_⟩
      intro σ
      exact ((Polynomial.natDegree_smul_le _ _).trans natDegree_map_le).trans_lt
        ((natDegree_minpolyDiv_lt (Algebra.IsIntegral.isIntegral x)).trans_le
          (minpoly.natDegree_le _))
    · rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
⊢ IsSepClosed k

Tactic:
by assumption

Goal state after:
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
⊢ (trace R S) ((algebraMap R S) x) = Fintype.card ι • x

Tactic:
have := Classical.decEq ι

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ (trace R S) ((algebraMap R S) x) = Fintype.card ι • x
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
⊢ (trace R S) ((trace S T) x) = (trace R T) x

Tactic:
have := Classical.decEq ι

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
this : DecidableEq ι
⊢ (trace R S) ((trace S T) x) = (trace R T) x
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case inl
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
x : R ⊗[k] K
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range

pp: case inr
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
x : R ⊗[k] K
a✝ : Nontrivial (R ⊗[k] K)
hq : q = 1
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
induction x with
  | zero => exact ⟨0, 0, by simp⟩
  | add x y h h' =>
    have : ExpChar (R ⊗[k] K) q := expChar_of_injective_ringHom (algebraMap k _).injective q
    simp_rw [RingHom.mem_range, ← RingHom.mem_rangeS, ← Subalgebra.mem_perfectClosure_iff] at h h' ⊢
    exact add_mem h h'
  | tmul x y =>
    obtain ⟨n, a, ha⟩ := IsPurelyInseparable.pow_mem k q y
    use n
    have : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) =
        (x ^ q ^ n) ⊗ₜ[k] (1 : K) * (1 : R) ⊗ₜ[k] (y ^ q ^ n) := by
      rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
    rw [Algebra.TensorProduct.tmul_pow, this]
    refine Subring.mul_mem _ ⟨x ^ q ^ n, rfl⟩ ⟨algebraMap k R a, ?_⟩
    rw [← IsScalarTower.algebraMap_apply, Algebra.TensorProduct.algebraMap_apply,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, ha]

Goal state after:
case inr
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
x : R ⊗[k] K
a✝ : Nontrivial (R ⊗[k] K)
hq : q = 1
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁵ : Group G
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x : A
x✝ : G
⊢ x✝ • (algebraMap A B) x = (algebraMap A B) x

Tactic:
by rw [smul_algebraMap]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
h : ∃ g ∈ Finset.univ, g • b ∈ P
⊢ b ∈ ⋃ i ∈ ↑⊤, ↑(i • P)

Tactic:
obtain ⟨g, -, hg⟩ := h

Goal state after:
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
g : ?m.146
hg : g • b ∈ P
⊢ b ∈ ⋃ i ∈ ↑⊤, ↑(i • P)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑n ∣ x.valMinAbs - y

Tactic:
← intCast_zmod_eq_zero_iff_dvd,

Goal state after:
case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑(x.valMinAbs - y) = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case hfg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : { x // x ∈ (minpoly K pb.gen).aroots E }), ?f✝ x = _root_.id ↑x

Tactic:
intro x; rfl

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

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
a : Kˣ
⊢ a ∈ univ.erase (-1) → a⁻¹ ∈ univ.erase (-1)

Tactic:
simp [@inv_eq_iff_eq_inv _ _ a]

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

Goal state before:
pp: A : Type u
B : Type v
C : Type z
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : CommRing C
inst✝ : Algebra A C
pb : PowerBasis A B
e : Fin pb.dim ≃ (B →ₐ[A] C)
⊢ embeddingsMatrixReindex A C (⇑pb.basis) e = (vandermonde fun i ↦ (e i) pb.gen)ᵀ

Tactic:
by
  ext i j
  simp [embeddingsMatrixReindex, embeddingsMatrix]

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

Goal state before:
pp: case refine_2
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ ((LinearMap.BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠ 0

Tactic:
simpa only [traceMatrix_of_basis] using det_traceMatrix_ne_zero' pb

Goal state after:
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ Associated a b

Tactic:
refine Int.natAbs_eq_natAbs_iff.trans ?_

Goal state after:
a b : ℤ
⊢ a = b ∨ a = -b ↔ Associated a b
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: case mpr.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))

Tactic:
exact Or.inr (by simp)

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

Goal state before:
pp: a : ℤ
⊢ Ideal.span {↑a.natAbs} = Ideal.span {a}

Tactic:
rw [Ideal.span_singleton_eq_span_singleton]

Goal state after:
a : ℤ
⊢ Associated (↑a.natAbs) a
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ↑a.valMinAbs.natAbs ^ 2 + ↑b.valMinAbs.natAbs ^ 2 ≡ x [ZMOD ↑p]

Tactic:
rw [← a.coe_valMinAbs, ← b.coe_valMinAbs] at hx

Goal state after:
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x
⊢ ↑a.valMinAbs.natAbs ^ 2 + ↑b.valMinAbs.natAbs ^ 2 ≡ x [ZMOD ↑p]
Module: Mathlib.RingTheory.ZMod

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = g
⊢ f = RingHom.comp ?m.65 f

pp: n : ℕ
R : Type u_1
inst✝ : Ring R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = g
⊢ ZMod n →+* ZMod n

Tactic:
RingHom.id_comp

Goal state after:
n : ℕ
R : Type u_1
inst✝ : Ring R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = g
⊢ f = f
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ.zero
p a d k : ℕ
hk : k ∈ range p
hd : p * a = d
⊢ p ∣ (p ^ 0 * d) ^ k * ↑(p.choose (k + 1))

Tactic:
cases k

Goal state after:
case succ.zero.zero
p a d : ℕ
hd : p * a = d
hk : 0 ∈ range p
⊢ p ∣ (p ^ 0 * d) ^ 0 * ↑(p.choose (0 + 1))

case succ.zero.succ
p a d : ℕ
hd : p * a = d
n✝ : ℕ
hk : n✝ + 1 ∈ range p
⊢ p ∣ (p ^ 0 * d) ^ (n✝ + 1) * ↑(p.choose (n✝ + 1 + 1))
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ.succ
p a d k : ℕ
hk : k ∈ range p
n✝ : ℕ
hd : (1 + p * a) ^ p ^ (n✝ + 1) = p ^ (n✝ + 1) * d + 1
⊢ p ∣ (p ^ (n✝ + 1) * d) ^ k * ↑(p.choose (k + 1))

Tactic:
cases k

Goal state after:
case succ.succ.zero
p a d n✝ : ℕ
hd : (1 + p * a) ^ p ^ (n✝ + 1) = p ^ (n✝ + 1) * d + 1
hk : 0 ∈ range p
⊢ p ∣ (p ^ (n✝ + 1) * d) ^ 0 * ↑(p.choose (0 + 1))

case succ.succ.succ
p a d n✝¹ : ℕ
hd : (1 + p * a) ^ p ^ (n✝¹ + 1) = p ^ (n✝¹ + 1) * d + 1
n✝ : ℕ
hk : n✝ + 1 ∈ range p
⊢ p ∣ (p ^ (n✝¹ + 1) * d) ^ (n✝ + 1) * ↑(p.choose (n✝ + 1 + 1))
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this✝ : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis ι R ↥N := smithNormalFormBotBasis b h
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
x : M
this : ∀ (c : ι → R) (i : ι), (b'.repr (∑ j, c j • a j • b' j)) i = a i * c i
c : ι → R
hc : ∀ (i : ι), (b'.repr x) i = a i * c i
⊢ ∃ c, x = ∑ x, c x • smithNormalFormCoeffs b h x • (smithNormalFormTopBasis b h) x

Tactic:
exact ⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩

Goal state after: