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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Module.finrank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (CotangentSpace (AdicCompletion (maximalIdeal R) R)) =
    Module.finrank (IsLocalRing.ResidueField R) (CotangentSpace R)

Tactic:
eq_comm

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Module.finrank (IsLocalRing.ResidueField R) (CotangentSpace R) =
    Module.finrank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (CotangentSpace (AdicCompletion (maximalIdeal R) R))
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ ↑f (degree x + 1) =
    (AdicCompletion.transitionMap (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) ⋯)
      ((Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) (Quotient.out (↑f n)))

Tactic:
eq_comm

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ (AdicCompletion.transitionMap (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) ⋯)
      ((Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) (Quotient.out (↑f n))) =
    ↑f (degree x + 1)
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : ↑(x m) m = ↑(x n) m
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m

Tactic:
eq_comm

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : ↑(x n) m = ↑(x m) m
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
⊢ Injective val

Tactic:
rintro ⟨a, ha⟩

Goal state after:
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ ∀ ⦃a₂ : GroupLike R A⦄, ↑{ val := a, isGroupLikeElem_val := ha } = ↑a₂ → { val := a, isGroupLikeElem_val := ha } = a₂
Module: Mathlib.RingTheory.Flat.Domain

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
⊢ Injective ⇑(map f g)

Tactic:
let K := FractionRing R
  refine .of_comp (f := TensorProduct.mk R K _ 1) ?_
  have H₁ := TensorProduct.map_injective_of_flat_flat (f.baseChange K) (g.baseChange K)
    (Module.Flat.lTensor_preserves_injective_linearMap f hf)
    (Module.Flat.lTensor_preserves_injective_linearMap g hg)
  have H₂ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm.injective
  have H₃ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N).injective
  have H₄ := (AlgebraTensorModule.assoc R R K K P Q).symm.injective
  have H₅ := (AlgebraTensorModule.assoc R R K K M N).injective
  have H₆ := Module.Flat.rTensor_preserves_injective_linearMap (M := P ⊗[R] Q)
    (Algebra.linearMap R K) (FaithfulSMul.algebraMap_injective R K)
  have H₇ := (TensorProduct.lid R (P ⊗[R] Q)).symm.injective
  convert! H₅.comp <| H₃.comp <| H₁.comp <| H₂.comp <| H₄.comp <| H₆.comp <| H₇
  dsimp only [← LinearMap.coe_comp, ← LinearEquiv.coe_toLinearMap,
    ← @LinearMap.coe_restrictScalars R K]
  congr! 1
  ext p q
  -- `simp` solves the goal but it times out
  change (1 : K) ⊗ₜ[R] (f p ⊗ₜ[R] g q) = (AlgebraTensorModule.assoc R R K K M N)
    (((1 : K) • (algebraMap R K) 1 ⊗ₜ[R] f p) ⊗ₜ[R] g q)
  simp only [map_one, one_smul, AlgebraTensorModule.assoc_tmul]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ ⊤ ≤
    Submodule.comap
      (ModuleCat.Hom.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂ ≫ (shortComplexH1 A).pOpcycles))
      (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles)).range

Tactic:
intro x _

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂
a✝ : x ∈ ⊤
⊢ x ∈
    Submodule.comap
      (ModuleCat.Hom.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂ ≫ (shortComplexH1 A).pOpcycles))
      (ModuleCat.Hom.hom ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles)).range
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ C (Submodule.IsPrincipal.generator p.contentIdeal) ∣ p

Tactic:
rw [C_dvd_iff_dvd_coeff]
  exact fun i ↦ h_prin.contentIdeal_generator_dvd_coeff i

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : Ideal R
inst✝ : p.IsPrime
ass : p ∈ associatedPrimes R M
⊢ maximalIdeal (Localization.AtPrime p) ∈ associatedPrimes (Localization.AtPrime p) (LocalizedModule.AtPrime p M)

Tactic:
by
  apply mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule
    p.primeCompl (LocalizedModule.mkLinearMap p.primeCompl M)
  simpa [Localization.AtPrime.under_maximalIdeal] using ass

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v' i' : R
vi✝ : (algebraMap R K) v' * (algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : (algebraMap R K) i' * (algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  (powMonoidHom n) { val := (algebraMap R K) v', inv := (algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  (algebraMap R K) (v' ^ n) = (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := (algebraMap R K) i', inv := (algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ (powMonoidHom n) { val := v', inv := i', val_inv := vi, inv_val := iv } =
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }

Tactic:
simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
         FaithfulSMul.algebraMap_injective R K hv

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
x✝ : A
ha : x✝ ∈ ⊥
⊢ (if x✝ = 0 ∧ 0 = 0 then 1 else 0) = 1

Tactic:
mem_bot.mp ha

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
x✝ : A
ha : x✝ ∈ ⊥
⊢ (if 0 = 0 ∧ 0 = 0 then 1 else 0) = 1
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : a ∈ ⊥
⊢ (if (if a = 0 ∧ n = 0 then 1 else 0) = 0 ∧ m = 0 then 1 else 0) =
    ↑(m.uniformBell n) * if a = 0 ∧ m * n = 0 then 1 else 0

Tactic:
mem_bot.mp ha

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : a ∈ ⊥
⊢ (if (if 0 = 0 ∧ n = 0 then 1 else 0) = 0 ∧ m = 0 then 1 else 0) =
    ↑(m.uniformBell n) * if 0 = 0 ∧ m * n = 0 then 1 else 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ x_1 ∈ univ.sigma fun a ↦ s.sym (n - ↑a), dpow (↑x_1.fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑x_1.snd) (x i) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)

Tactic:
eq_comm

Goal state after:
case insert
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i) =
    ∑ x_1 ∈ univ.sigma fun a ↦ s.sym (n - ↑a), dpow (↑x_1.fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑x_1.snd) (x i)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
n : ℕ
⊢ f (r ^ n) * f (hI.dpow n x) = hJ.dpow n (f r * f x)

Tactic:
map_pow,

Goal state after:
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
n : ℕ
⊢ f r ^ n * f (hI.dpow n x) = hJ.dpow n (f r * f x)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
n : ℕ
⊢ f (hI.dpow n (r • x)) = hJ.dpow n (f (r • x))

Tactic:
rw [smul_eq_mul, hI.dpow_mul hx.1, map_mul, map_mul, map_pow,
      hJ.dpow_mul (hf (mem_map_of_mem f hx.1)), hx.2 n]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
⊢ ⇑f '' S ⊆ ↑J

Tactic:
rintro b ⟨a, has, rfl⟩

Goal state after:
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
a : A
has : a ∈ S
⊢ f a ∈ ↑J
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
⊢ 0 =
    ∑ k ∈ Finset.antidiagonal m, (if x ∈ I then (↑k.1!)⁻¹ʳ * x ^ k.1 else 0) * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0

Tactic:
eq_comm

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
⊢ (∑ k ∈ Finset.antidiagonal m,
      (if x ∈ I then (↑k.1!)⁻¹ʳ * x ^ k.1 else 0) * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0) =
    0
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ (k.1 + k.2))

Tactic:
add_comm,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ y ^ k.2 * x ^ k.1 ∈ ↑(I ^ (k.2 + k.1))
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
h : a + b = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
add_comm,

Goal state after:
R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
h : b + a = 1
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⨆ a ∈ S, ↑a = ⨆ a ∈ Set.range fun a ↦ ⨆ (_ : a ∈ S), ⟨a.carrier, ⋯⟩, ↑a

Tactic:
iSup_range

Goal state after:
case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⨆ a ∈ S, ↑a = ⨆ i, ↑(⨆ (_ : i ∈ S), ⟨i.carrier, ⋯⟩)
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
ι : Type u_4
inst✝ : Finite ι
⊢ ∃ n, Nonempty ((ι → R) ≃ₐ[R] Fin n → R)

Tactic:
cases nonempty_fintype ι
    exact ⟨_, ⟨AlgEquiv.piCongrLeft' _ _ (Fintype.equivFin ι)⟩⟩

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Subsingleton R
⊢ IsFiniteSplit R S

Tactic:
have : Subsingleton S := RingHom.codomain_trivial (algebraMap R S)

Goal state after:
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Subsingleton R
this : Subsingleton S
⊢ IsFiniteSplit R S
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv ∘ₗ h1Cotangentι =
    H1Cotangent.δ R P.Ring S ∘ₗ ↑P.h1CotangentExtendScalarsEquiv

Tactic:
h1CotangentExtendScalarsEquiv_toLinearMap

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ P.cotangentComplex ∘ₗ ↑P.cotangentExtendScalarsEquiv ∘ₗ h1Cotangentι =
    H1Cotangent.δ R P.Ring S ∘ₗ H1Cotangent.map (Hom.ofAlgHom (ofId P.Ring (Generators.self P.Ring S).Ring) ⋯)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
⊢ (if h : ∃ a, f ↑a = x then f (hI.dpow n ↑(Classical.choose h)) else 0 x) = 0

Tactic:
dif_neg,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
⊢ 0 x = 0

case hnc
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
⊢ ¬∃ a, f ↑a = x
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
a : A
ha : a ∈ I
hax : f a = x
⊢ dpow hI f 1 x = x

Tactic:
← hax,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
a : A
ha : a ∈ I
hax : f a = x
⊢ dpow hI f 1 (f a) = f a
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
τ : ↑(P.primesOver S) → G
hτ : ∀ (Q' : ↑(P.primesOver S)), ↑Q' = τ Q' • Q
σ : G
hσ : IsArithFrobAt R σ Q
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Tactic:
refine ⟨fun Q' ↦ τ Q' * σ * (τ Q')⁻¹, fun Q' ↦ hτ Q' ▸ hσ.conj (τ Q'), fun Q₁ Q₂ ↦
    .trans (.symm (isConj_iff.mpr ⟨τ Q₁, rfl⟩)) (isConj_iff.mpr ⟨τ Q₂, rfl⟩)⟩

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
G : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulSemiringAction G S
inst✝⁶ : SMulCommClass G R S
Q : Ideal S
inst✝⁵ : Finite G
inst✝⁴ : Algebra.IsInvariant R S G
inst✝³ : Q.IsPrime
inst✝² : Finite (S ⧸ Q)
Q' : Ideal S
inst✝¹ : Q'.IsPrime
inst✝ : Finite (S ⧸ Q')
H : Ideal.under R Q = Ideal.under R Q'
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
⊢ arithFrobAt R G Q = ⋯.choose ⟨Q, ⋯⟩

pp: case e'_4
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
G : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulSemiringAction G S
inst✝⁶ : SMulCommClass G R S
Q : Ideal S
inst✝⁵ : Finite G
inst✝⁴ : Algebra.IsInvariant R S G
inst✝³ : Q.IsPrime
inst✝² : Finite (S ⧸ Q)
Q' : Ideal S
inst✝¹ : Q'.IsPrime
inst✝ : Finite (S ⧸ Q')
H : Ideal.under R Q = Ideal.under R Q'
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
⊢ arithFrobAt R G Q' = ⋯.choose ⟨Q', ⋯⟩

Tactic:
· subst h₁; rfl

Goal state after:
case e'_4
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
G : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulSemiringAction G S
inst✝⁶ : SMulCommClass G R S
Q : Ideal S
inst✝⁵ : Finite G
inst✝⁴ : Algebra.IsInvariant R S G
inst✝³ : Q.IsPrime
inst✝² : Finite (S ⧸ Q)
Q' : Ideal S
inst✝¹ : Q'.IsPrime
inst✝ : Finite (S ⧸ Q')
H : Ideal.under R Q = Ideal.under R Q'
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
⊢ arithFrobAt R G Q' = ⋯.choose ⟨Q', ⋯⟩
Module: Mathlib.RingTheory.PowerSeries.Binomial

Goal state before:
pp: case succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose n) = ↑(↑(↑n).negOnePow • Ring.choose (↑d + ↑n) n)

Tactic:
← Nat.cast_add,

Goal state after:
case succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose n) = ↑(↑(↑n).negOnePow • Ring.choose (↑(d + n)) n)
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))

Tactic:
by_cases hz : n = 0

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : n = 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))

case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : ¬n = 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
⊢ (Equiv e s).hsum = s.hsum

Tactic:
ext g
  simp only [coeff_hsum, Equiv_toFun]
  exact finsum_eq_of_bijective e.symm (Equiv.bijective e.symm) fun x => rfl

Goal state after: