mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h.zero
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
x : M
h' : x ∈ φ.maxGenEigenspace 0
⊢ ↑((restrict φ hφV ^ 0) ⟨x, h'⟩) = (φ ^ 0) x

Tactic:
simp [pow_succ', *]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h.succ
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
x : M
h' : x ∈ φ.maxGenEigenspace 0
n✝ : ℕ
a✝ : ↑((restrict φ hφV ^ n✝) ⟨x, h'⟩) = (φ ^ n✝) x
⊢ ↑((restrict φ hφV ^ (n✝ + 1)) ⟨x, h'⟩) = (φ ^ (n✝ + 1)) x

Tactic:
simp [pow_succ', *]

Goal state after:
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x : L
⊢ χ 0 = 0

Tactic:
exact map_zero _

Goal state after:
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : Invertible P
A : ↥(skewAdjointMatricesLieSubalgebra J)
⊢ ↑((skewAdjointMatricesLieSubalgebraEquiv J P h) A) = P⁻¹ * ↑A * P

Tactic:
by
  simp [skewAdjointMatricesLieSubalgebraEquiv]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ (J l R)ᵀ = -J l R

Tactic:
rw [J, fromBlocks_transpose, ← neg_one_smul R (fromBlocks _ _ _ _ : Matrix (l ⊕ l) (l ⊕ l) R),
    fromBlocks_smul, Matrix.transpose_zero, Matrix.transpose_one, transpose_neg]
  simp [fromBlocks]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝⁵ : DecidableEq l
inst✝⁴ : Fintype l
inst✝³ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
F : Type u_3
S : Type u_4
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
hA : A ∈ symplecticGroup l R
f : F
⊢ A.map ⇑f ∈ symplecticGroup l S

Tactic:
simp_rw [mem_iff, ← transpose_map, ← map_J _ f, ← Matrix.map_mul, mem_iff.mp hA]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ -Aᵀ * (J l R)⁻¹ * A = -Aᵀ * (A * J l R * Aᵀ)⁻¹ * A

Tactic:
rw [hA]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ * J l R * A = J l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R

Tactic:
rw [hA]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: case refine_2
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A B C D : Matrix l l R
h : Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1
⊢ (fromBlocks A B C D)ᵀ * J l R * fromBlocks A B C D = J l R

Tactic:
· simp only [fromBlocks_transpose, J, fromBlocks_multiply, mul_zero, mul_one, zero_add, mul_neg,
      add_zero, neg_mul, ← sub_eq_add_neg, fromBlocks_inj, sub_eq_zero]
    exact ⟨h.1.symm, by grind, by simpa using congr(transpose $(h.2.2)), h.2.1.symm⟩

Goal state after:
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z = 0
⊢ ∃ m, m ≠ 0 ∧ ((toEnd K ↥U ↥E) (α • u + x')) m = 0

Tactic:
refine ⟨⟨x, self_mem_engel K x⟩, ?_, ?_⟩
      · exact Subtype.coe_ne_coe.mp hx₀
      · dsimp only [z] at hz₀
        simp only [hz₀, map_zero, LinearMap.zero_apply]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ a.coeff.support ⊆ {m}

Tactic:
rw [← Finset.coe_subset, Finset.coe_singleton]
  rfl

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ GradedMonoid.mk (f (Multiplicative.toAdd 1)) ⟨single (Multiplicative.toAdd 1) 1, ⋯⟩ =
    GradedMonoid.mk 0 GradedMonoid.GOne.one

Tactic:
congr 2 <;> simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case refine_1
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
hx : 0 ∈ gradeBy R (⇑f) i
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨0, hx⟩ = (decomposeAux f) ↑⟨0, hx⟩

Tactic:
exact map_zero _

Goal state after:
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, ⁅x✝¹.left, x✝.left⁆⁆ + ⁅x✝².left, (ψ x✝¹.right) x✝.left⁆ - ⁅x✝².left, (ψ x✝.right) x✝¹.left⁆ +
        (⁅x✝¹.left, (ψ x✝².right) x✝.left⁆ - ⁅x✝.left, (ψ x✝².right) x✝¹.left⁆ + (ψ x✝².right) ((ψ x✝¹.right) x✝.left) -
          (ψ x✝².right) ((ψ x✝.right) x✝¹.left)) -
      ((ψ x✝¹.right) ((ψ x✝.right) x✝².left) - (ψ x✝.right) ((ψ x✝¹.right) x✝².left)) =
    ⁅x✝².left, ⁅x✝¹.left, x✝.left⁆⁆ - ⁅x✝¹.left, ⁅x✝².left, x✝.left⁆⁆ + ⁅(ψ x✝².right) x✝¹.left, x✝.left⁆ -
            ⁅(ψ x✝¹.right) x✝².left, x✝.left⁆ +
          ((ψ x✝².right) ((ψ x✝¹.right) x✝.left) - (ψ x✝¹.right) ((ψ x✝².right) x✝.left)) -
        (⁅x✝².left, (ψ x✝.right) x✝¹.left⁆ - ⁅x✝¹.left, (ψ x✝.right) x✝².left⁆ + (ψ x✝.right) ((ψ x✝².right) x✝¹.left) -
          (ψ x✝.right) ((ψ x✝¹.right) x✝².left)) +
      (⁅x✝¹.left, ⁅x✝².left, x✝.left⁆⁆ + ⁅x✝¹.left, (ψ x✝².right) x✝.left⁆ - ⁅x✝¹.left, (ψ x✝.right) x✝².left⁆ +
          (⁅x✝².left, (ψ x✝¹.right) x✝.left⁆ - ⁅x✝.left, (ψ x✝¹.right) x✝².left⁆ +
              (ψ x✝¹.right) ((ψ x✝².right) x✝.left) -
            (ψ x✝¹.right) ((ψ x✝.right) x✝².left)) -
        ((ψ x✝².right) ((ψ x✝.right) x✝¹.left) - (ψ x✝.right) ((ψ x✝².right) x✝¹.left)))

Tactic:
grind [lie_skew]

Goal state after:
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² : R
x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝¹, x✝² • x✝⁆ = x✝² • ⁅x✝¹, x✝⁆

Tactic:
simp [smul_sub, smul_add]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p.toList x)[k] = y
⊢ (p ^ ((k + 1) % (p.toList x).length)) x = (p * p ^ k) x

Tactic:
← pow_succ'

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p.toList x)[k] = y
⊢ (p ^ ((k + 1) % (p.toList x).length)) x = (p ^ (k + 1)) x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
⊢ l.formPerm.support = l.toFinset

Tactic:
refine support_formPerm_of_nodup _ hn ?_

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
⊢ ∀ (x : α), l ≠ [x]
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
hx : x ∈ f.toCycle hf
l : α
hl : f.toCycle hf = ↑(f.toList l)
⊢ (f.toCycle hf).next ⋯ x hx = f x

Tactic:
simp only [hl, Cycle.mem_coe_iff] at ⊢ hx

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
hx✝ : x ∈ f.toCycle hf
l : α
hl : f.toCycle hf = ↑(f.toList l)
hx : x ∈ f.toList l
⊢ (↑(f.toList l)).next ⋯ x ⋯ = f x
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
hx : x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s
⊢ x ∈ s

Tactic:
rw [Finset.mem_union]

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
hx : x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s
⊢ x ∈ (F f).support ∨ x ∈ Finset.image (⇑(Equiv.neg A)) (F f).support
Module: Mathlib.Algebra.Lie.SerreConstruction

Goal state before:
pp: R : Type u
B : Type v
inst✝ : CommRing R
CM : Matrix B B ℤ
i : B
h : CM i i = 2
⊢ adE R CM (i, i) = 0

Tactic:
have h' : (-2 : ℤ).toNat = 0 := rfl
  simp [adE, h, h']

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = p * ↑ha.unit⁻¹

Tactic:
by rw [hab, mul_assoc, IsUnit.mul_val_inv ha, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : IsDomain R
inst✝¹ : Module.IsTorsionFree R P
inst✝ : Nontrivial P
I : FractionalIdeal S P
h_nz : ↑I.den ≠ 0
x : ↥I
⊢ (Algebra.linearMap R P)
      ↑((equivMapOfInjective (Algebra.linearMap R P) ⋯ I.num).symm ⟨(DistribSMul.toLinearMap R P I.den) ↑x, ⋯⟩) =
    I.den • ↑x

Tactic:
Submodule.map_equivMapOfInjective_symm_apply,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : IsDomain R
inst✝¹ : Module.IsTorsionFree R P
inst✝ : Nontrivial P
I : FractionalIdeal S P
h_nz : ↑I.den ≠ 0
x : ↥I
⊢ ↑⟨(DistribSMul.toLinearMap R P I.den) ↑x, ⋯⟩ = I.den • ↑x
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I : FractionalIdeal S P
g : P ≃ₐ[R] P'
⊢ map (↑g.symm) (map (↑g) I) = I

Tactic:
← map_comp,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I : FractionalIdeal S P
g : P ≃ₐ[R] P'
⊢ map ((↑g.symm).comp ↑g) I = I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I : FractionalIdeal S P'
g : P ≃ₐ[R] P'
⊢ map (↑g) (map (↑g.symm) I) = I

Tactic:
← map_comp,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I : FractionalIdeal S P'
g : P ≃ₐ[R] P'
⊢ map ((↑g).comp ↑g.symm) I = I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
P'' : Type u_4
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
I✝ J : FractionalIdeal S P
g✝ : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P
⊢ map (↑g.symm) (map (↑g) I) = I

Tactic:
← map_comp,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
P'' : Type u_4
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
I✝ J : FractionalIdeal S P
g✝ : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P
⊢ map ((↑g.symm).comp ↑g) I = I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
P'' : Type u_4
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
I✝ J : FractionalIdeal S P
g✝ : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P'
⊢ map (↑g) (map (↑g.symm) I) = I

Tactic:
← map_comp,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
P'' : Type u_4
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
I✝ J : FractionalIdeal S P
g✝ : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P'
⊢ map ((↑g).comp ↑g.symm) I = I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
inj : Function.Injective ⇑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ I.FG

Tactic:
rw [← coeIdeal_fg S inj I]

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
inj : Function.Injective ⇑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ (↑↑I).FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ : ∀ x ∈ {Z | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥}, ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hIM : I ≤ P.asIdeal
hM : P.asIdeal.IsMaximal
hPM : P.asIdeal ≤ P.asIdeal
⊢ (P.asIdeal ::ₘ Multiset.map asIdeal (Z.erase P)).prod ≤ I

Tactic:
convert! hZI

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ : ∀ x ∈ {Z | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥}, ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hIM : I ≤ P.asIdeal
hM : P.asIdeal.IsMaximal
hPM : P.asIdeal ≤ P.asIdeal
⊢ P.asIdeal ::ₘ Multiset.map asIdeal (Z.erase P) = Multiset.map asIdeal Z
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥R⁰
x : R
hx : (algebraMap R K) x = ↑z • y
⊢ (algebraMap R K) x ∈ I

Tactic:
rw [hx]

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
I : FractionalIdeal R⁰ K
inst✝ : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥R⁰
x : R
hx : (algebraMap R K) x = ↑z • y
⊢ ↑z • y ∈ I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mp
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ ⟨↑I / ↑1, ⋯⟩
⊢ x✝ ∈ I

pp: case mpr
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
⊢ x✝ ∈ ⟨↑I / ↑1, ⋯⟩

Tactic:
· simpa using mem_div_iff_forall_mul_mem.mp h 1 ((algebraMap R₁ K).map_one ▸ coe_mem_one R₁⁰ 1)

Goal state after:
case mpr
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
⊢ x✝ ∈ ⟨↑I / ↑1, ⋯⟩
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (x y : K),
    x ∈ span R₁ (f '' ↑s) →
      y ∈ span R₁ (f '' ↑s) → IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • y) → IsInteger R₁ (↑a' • (x + y))

Tactic:
intro x y _ _ hx hy
      rw [smul_add]
      exact IsLocalization.isInteger_add hx hy

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
this : WellFoundedGT (Ideal A)
⊢ WellFounded DvdNotUnit

Tactic:
convert! this.wf using 3

Goal state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
this : WellFoundedGT (Ideal A)
x✝¹ x✝ : Ideal A
⊢ DvdNotUnit x✝¹ x✝ ↔ x✝ < x✝¹
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ ∀ {a : Ideal A}, Irreducible a ↔ Prime a

Tactic:
by
      intro P
      exact ⟨fun hirr => ⟨hirr.ne_zero, hirr.not_isUnit, fun I J => by
        have : P.IsMaximal := by
          refine ⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩
          intro J hJ
          obtain ⟨_J_ne, H, hunit, P_eq⟩ := Ideal.dvdNotUnit_iff_lt.mpr hJ
          exact Ideal.isUnit_iff.mp ((hirr.isUnit_or_isUnit P_eq).resolve_right hunit)
        rw [Ideal.dvd_iff_le, Ideal.dvd_iff_le, Ideal.dvd_iff_le, SetLike.le_def, SetLike.le_def,
          SetLike.le_def]
        contrapose!
        rintro ⟨⟨x, x_mem, x_notMem⟩, ⟨y, y_mem, y_notMem⟩⟩
        exact
          ⟨x * y, Ideal.mul_mem_mul x_mem y_mem,
            mt this.isPrime.mem_or_mem (not_or_intro x_notMem y_notMem)⟩⟩, Prime.irreducible⟩

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

Goal state before:
pp: R : Type u_1
inst✝²¹ : CommRing R
S : Type u_2
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : AddCommGroup M₂
inst✝¹⁶ : AddCommGroup M₃
inst✝¹⁵ : AddCommGroup N₁
inst✝¹⁴ : AddCommGroup N₂
inst✝¹³ : AddCommGroup N₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R N₁
inst✝⁸ : Module R N₂
inst✝⁷ : Module R N₃
inst✝⁶ : Module S N₁
inst✝⁵ : Module S N₂
inst✝⁴ : Module S N₃
inst✝³ : IsScalarTower R S N₁
inst✝² : IsScalarTower R S N₂
inst✝¹ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
inst✝ : Module.Flat R S
isb₂ : IsBaseChange S h₂
isb₃ : IsBaseChange S h₃
exact₁ : Function.Exact ⇑f ⇑g
inj₁ : Function.Injective ⇑f
exact₂ : Function.Exact ⇑f' ⇑g'
inj₂ : Function.Injective ⇑f'
⊢ IsBaseChange S h₁

Tactic:
simp only [IsBaseChange, IsTensorProduct] at isb₂ isb₃ ⊢
  refine LinearMap.bijective_of_bijective_of_injective_of_left_exact
    ((f.baseChange S).restrictScalars R) ((g.baseChange S).restrictScalars R)
    (f'.restrictScalars R) (g'.restrictScalars R) _ _ _ ?_ ?_ ?_ exact₂ isb₂ isb₃.1 ?_ inj₂
  · ext s m
    simpa using congr(s • ($comm₁ m)).symm
  · ext s m
    simpa using congr(s • ($comm₂ m)).symm
  · exact Module.Flat.lTensor_exact S exact₁
  · exact Module.Flat.lTensor_preserves_injective_linearMap f inj₁

Goal state after: