mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit (f x)
⊢ IsUnit x

Tactic:
by
    by_contra hx
    obtain ⟨p, hp, _⟩ := exists_max_ideal_of_mem_nonunits hx
    obtain ⟨⟨q, hqp⟩, hq⟩ := hf ⟨p, hp.isPrime⟩
    simp only [PrimeSpectrum.ext_iff, comap_asIdeal] at hq
    exact hqp.ne_top (q.eq_top_of_isUnit_mem (q.mem_comap.mp (by rwa [hq])) hfx)

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal A
⊢ (Ideal.comap (algebraMap R A) J).minimalPrimes = Ideal.comap (algebraMap R A) '' J.minimalPrimes

Tactic:
conv_rhs => rw [← map_under S A J, minimalPrimes_map S]
  refine (Set.image_preimage_eq_iff.mpr ?_).symm
  exact subset_trans (Ideal.minimalPrimes_comap_subset (algebraMap R A) J) (by simp)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∉ range ⇑(algebraMap R K) → ¬∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Tactic:
intro hrange hlocal

Goal state after:
case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
hlocal : ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
⊢ False
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ f ⁻¹' s' = s

Tactic:
by
  simp_rw [IsLocallyClosed, hf.isOpen_iff, hf.isClosed_iff]
  constructor
  · rintro ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩
    exact ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩
  · rintro ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩
    exact ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s✝ t : Set α
a b : α
L : BooleanSubalgebra α
s : Set α
hs : s = ↑L
⊢ s = ↑L.toSublattice

Tactic:
subst hs; rfl

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case refine_3
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t : Finset (↑s × ↑s)
⊢ ∃ t_1, (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
refine t.induction ⟨{(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}, by simp⟩ fun ⟨x, y⟩ t _ ⟨tc, eq⟩ ↦ ?_

Goal state after:
case refine_3
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝ : Finset (↑s × ↑s)
x✝² : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝¹ : ∃ t_1, (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝ : (x, y) ∉ t
tc : Finset (↑s × ↑s)
eq : (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ∃ t_1, ((insert (x, y) t).sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x ↦ ↑x.1 \ ↑x.2
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : (Opens α)ᵒᵈ
⊢ (⇑toDual ∘ compl) ((Opens.compl ∘ ⇑ofDual) s) = s

Tactic:
by simp [Opens.compl_compl]

Goal state after:
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Opens α
⊢ (Closeds.compl ∘ ⇑ofDual) ((⇑toDual ∘ compl) s) = s

Tactic:
by simp [Opens.compl_compl]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : QuasiSeparatedSpace β
h : IsOpenEmbedding f
⊢ QuasiSeparatedSpace α

Tactic:
by
  rw [← isQuasiSeparated_univ_iff, h.isQuasiSeparated_iff]
  exact isQuasiSeparated_univ.of_subset <| Set.subset_univ _

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : PartialOrder P
inst✝ : OrderTop P
a : P
⊢ (principal a).IsProper ↔ a ≠ ⊤

Tactic:
isProper_iff_top_notMem,

Goal state after:
P : Type u_1
inst✝¹ : PartialOrder P
inst✝ : OrderTop P
a : P
⊢ ⊤ ∉ principal a ↔ a ≠ ⊤
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
⊢ ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁

Tactic:
obtain ⟨x, hx⟩ := hU₂Z

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x : X
hx : x ∈ Z ∩ U₂
⊢ ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
hs : IsConstructible s
⊢ IsConstructible (f '' s)

Tactic:
by
  induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    have hfU : IsOpen (f '' U ∪ (range f)ᶜ) := by
      simpa [← range_sdiff_image hf.injective, sdiff_eq, compl_inter, union_comm]
        using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
    suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by
      simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)
    rintro V hVcomp hVopen
    rw [union_inter_distrib_right, ← image_inter_preimage]
    exact ((hUcomp (hf.isCompact_preimage hVcomp) (hVopen.preimage hf.continuous)).image
      hf.continuous).union <| hfcomp hVcomp hVopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_sdiff_image hf.injective]
    exact (hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs'

Goal state after:
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).FaithfullyFlat ↔ Module.FaithfullyFlat R S

Tactic:
by
  simp only [FaithfullyFlat]
  congr!
  exact Algebra.algebra_ext _ _ fun _ ↦ rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
h : D b = 0
⊢ ((b ^ 2)⁻¹ * b) • D a = b⁻¹ • D a

Tactic:
← mul_self_mul_inv b⁻¹,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a b : K
h : D b = 0
⊢ ((b ^ 2)⁻¹ * b) • D a = (b⁻¹ * b⁻¹ * b⁻¹⁻¹) • D a
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ (if h : ExponentExists G then Nat.find h else 0) ≤ n

Tactic:
dif_pos

Goal state after:
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ Nat.find ?hc ≤ n

case hc
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ ExponentExists G
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ⟨a, ⋯⟩ ^ (k % ↑(minimalPeriod (fun x ↦ a • x) b)) • ⟨b, ⋯⟩ = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩

Tactic:
exact Subtype.ext (zpow_smul_mod_minimalPeriod _ _ k)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ zeroLocus {e} = ↑(basicOpen f)

Tactic:
basicOpen_eq_zeroLocus_of_mul_add f e

Goal state after:
R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ zeroLocus {e} = zeroLocus {e}

case mul
R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ f * e = 0

case add
R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
⊢ f + e = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
this :
  ∀ x ∈ {e | IsIdempotentElem e}, ∀ y ∈ {e | IsIdempotentElem e}, basicOpen x = basicOpen y → x ≠ y → x * y ≠ x → False
ne' : ¬x * y ≠ x
⊢ x * y ≠ y

Tactic:
of_not_not ne'

Goal state after:
case inr
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
this :
  ∀ x ∈ {e | IsIdempotentElem e}, ∀ y ∈ {e | IsIdempotentElem e}, basicOpen x = basicOpen y → x ≠ y → x * y ≠ x → False
ne' : ¬x * y ≠ x
⊢ x ≠ y
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : H →* G
hf : IsPGroup p ↥f.ker
inst✝ : Finite (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P ↦ exists_comap_eq_of_ker_isPGroup P hf
g : Sylow p H → Sylow p G := fun P ↦ Classical.choose ⋯
hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P
P Q : Sylow p H
h : g P = g Q
⊢ ↑P = ↑Q

Tactic:
by rw [← hg, h]; exact (h_exists Q).choose_spec

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
⊢ ↑P ≤ centralizer ↑(zpowers x)

Tactic:
rwa [le_centralizer_iff, zpowers_le]

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsAddTorsion R
f : M
⊢ ∃ n, 0 < n ∧ n • f = 0

Tactic:
obtain ⟨n, npos, hn⟩ := (tR 1).exists_nsmul_eq_zero

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsAddTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ ∃ n, 0 < n ∧ n • f = 0
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
⊢ ¬IsCyclic α ↔ exponent α = p

Tactic:
refine ⟨fun h_cyc ↦ (Monoid.exponent_eq_prime_iff hp).mpr fun g hg ↦ ?_, fun h_exp h_cyc ↦ by
    obtain (rfl | rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm
    · exact Nat.not_prime_zero hp
    · exact Nat.not_prime_one hp⟩

Goal state after:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
⊢ orderOf g = p
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
a : Bool
⊢ a = ⊥ ∨ a = ⊤

Tactic:
rw [← Finset.mem_singleton, Or.comm, ← Finset.mem_insert, top_eq_true, bot_eq_false, ←
      Fintype.univ_bool]
    apply Finset.mem_univ

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : ∀ (x : G'), x ∈ zpowers g'
h : orderOf g = orderOf g'
⊢ (monoidHomOfForallMemZpowers hg ⋯).comp (monoidHomOfForallMemZpowers hg' ⋯) = MonoidHom.id G'

Tactic:
by simp [MonoidHom.eq_iff_eq_on_generator hg']

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
⊢ ∀ (s : ι → ↑(Iic a)), b ≤ iSup s → ∃ t, b ≤ ⨆ a_2 ∈ t, s a_2

Tactic:
s

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
⊢ b ≤ iSup s → ∃ t, b ≤ ⨆ a_2 ∈ t, s a_2
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1

Tactic:
obtain ⟨t, ht⟩ := h ι ((↑) ∘ s) hb

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
t : Finset ι
ht : ↑b ≤ ⨆ a_1 ∈ t, (Subtype.val ∘ s) a_1
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
⊢ ComplementedLattice α

Tactic:
apply complementedLattice_of_sSup_atoms_eq_top
  have : ∀ i ∈ s, ∃ t : Set α, f i = sSup t ∧ ∀ a ∈ t, IsAtom a := fun i hi ↦ by
    replace h := complementedLattice_iff_isAtomistic.mp (h i hi)
    obtain ⟨u, hu, hu'⟩ := eq_sSup_atoms (⊤ : Iic (f i))
    refine ⟨(↑) '' u, ?_, ?_⟩
    · replace hu : f i = ↑(sSup u) := Subtype.ext_iff.mp hu
      simp_rw [hu, Iic.coe_sSup]
    · rintro b ⟨⟨a, ha'⟩, ha, rfl⟩
      exact IsAtom.of_isAtom_coe_Iic (hu' _ ha)
  choose t ht ht' using this
  let u : Set α := ⋃ i, ⋃ hi : i ∈ s, t i hi
  have hu₁ : u ⊆ {a | IsAtom a} := by
    rintro a ⟨-, ⟨i, rfl⟩, ⟨-, ⟨hi, rfl⟩, ha : a ∈ t i hi⟩⟩
    exact ht' i hi a ha
  have hu₂ : sSup u = ⨆ i ∈ s, f i := by simp_rw [u, sSup_iUnion, biSup_congr' ht]
  rw [eq_top_iff, ← h', ← hu₂]
  exact sSup_le_sSup hu₁

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : ↑P = ⊥
⊢ p ∣ 1

Tactic:
have key : p ∣ Nat.card P := P.dvd_card_of_dvd_card hdvd

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : ↑P = ⊥
key : p ∣ Nat.card ↥↑P
⊢ p ∣ 1
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
⊢ Equivalent (snoc s₁ x₁ hsat₁) (snoc s₂ x₂ hsat₂)

Tactic:
refine ⟨e, fun i => ?_⟩

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc, (snoc s₁ x₁ hsat₁).toFun i.succ)
    ((snoc s₂ x₂ hsat₂).toFun (e i).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i).succ)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: M : Type u_4
inst✝² : AddCommGroup M
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R M
simple : IsSimpleModule R M
⊢ (Module.annihilator R M).IsMaximal

Tactic:
have ⟨I, max, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp simple

Goal state after:
M : Type u_4
inst✝² : AddCommGroup M
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R M
simple : IsSimpleModule R M
I : Ideal R
max : I.IsMaximal
e : M ≃ₗ[R] R ⧸ I
⊢ (Module.annihilator R M).IsMaximal
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
⊢ ∃ t, head t = head s ∧ t.length + 1 = n + 1 ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)

Tactic:
· have imxs : IsMaximal (x ⊓ s.eraseLast.last) s.eraseLast.last :=
        isMaximal_of_eq_inf x s.last rfl (Ne.symm hetx) hm (isMaximal_eraseLast_last h0s)
      have := ih _ _ imxs (le_inf (by simpa) (le_last_of_mem s.eraseLast.head_mem)) (by simp [hn])
      rcases this with ⟨t, htb, htl, htt, hteqv⟩
      have hmtx : IsMaximal t.last x :=
        isMaximal_of_eq_inf s.eraseLast.last s.last (by rw [inf_comm, htt]) hetx
          (isMaximal_eraseLast_last h0s) hm
      use snoc t x hmtx
      refine ⟨by simp [htb], by simp [htl], by simp, ?_⟩
      have : s.Equivalent ((snoc t s.eraseLast.last <| show IsMaximal t.last _ from
        htt.symm ▸ imxs).snoc s.last
          (by simpa using isMaximal_eraseLast_last h0s)) := by
        conv_lhs => rw [eq_snoc_eraseLast h0s]
        exact Equivalent.snoc hteqv (by simpa using iso_refl)
      refine this.trans <| Equivalent.snoc_snoc_swap
        (iso_symm
            (second_iso_of_eq hm
              (sup_eq_of_isMaximal hm (isMaximal_eraseLast_last h0s) (Ne.symm hetx)) htt.symm))
        (second_iso_of_eq (isMaximal_eraseLast_last h0s)
            (sup_eq_of_isMaximal (isMaximal_eraseLast_last h0s) hm hetx) (by rw [inf_comm, htt]))

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
⊢ ∀ n_1 ∈ I ^ n, (monomial (n + 1)) (r • n_1) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
s

Goal state after:
case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
⊢ s ∈ I ^ n → (monomial (n + 1)) (r • s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : single R j '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
hj' : n₀ ≤ j
⊢ single R (j + 1) '' ↑(I • F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))

Tactic:
rintro _ ⟨m, hm, rfl⟩

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : single R j '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • F.N j)
⊢ single R (j + 1) m ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ Monotone fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))

Tactic:
intro n m e

Goal state after:
case mp.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
⊢ (fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))) n ≤
    (fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))) m
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this✝ : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
this : y + z ∈ J
zmemJ : z ∈ J
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))

Tactic:
have xeq : x = J.toCotangent ⟨z, zmemJ⟩ := by simpa [← hx', J.toCotangent_eq, ← hyz] using hy

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this✝ : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
this : y + z ∈ J
zmemJ : z ∈ J
xeq : x = J.toCotangent ⟨z, zmemJ⟩
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
P : ModuleCat R
inst✝⁵ : Small.{v, u} R
inst✝⁴ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝³ : AddCommGroup M✝
inst✝² : AddCommGroup N✝
inst✝¹ : Module R M✝
inst✝ : Module R N✝
f : M✝ →ₗ[R] N✝
g : ↑P →ₗ[R] N✝
⊢ Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g

Tactic:
s

Goal state after:
R : Type u
inst✝⁶ : Ring R
P : ModuleCat R
inst✝⁵ : Small.{v, u} R
inst✝⁴ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝³ : AddCommGroup M✝
inst✝² : AddCommGroup N✝
inst✝¹ : Module R M✝
inst✝ : Module R N✝
f : M✝ →ₗ[R] N✝
g : ↑P →ₗ[R] N✝
s : Function.Surjective ⇑f
⊢ ∃ h, f ∘ₗ h = g
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (if h : ∃ j, c.Rel i j then h.choose else i)

Tactic:
dif_pos

Goal state after:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (Exists.choose ?hc)

case hc
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ ∃ j, c.Rel i j