mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ b = (a + c) * b

Tactic:
by rw [add_ac, one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : I ≤ comap (algebraMap R (Localization.AtPrime p)) q
hq : q.IsPrime
h₁ : (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p) ⟨q, hq⟩)).IsPrime
h₂ : ↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p) ⟨q, hq⟩) ≤ p
⊢ p ≤ comap (algebraMap R (Localization.AtPrime p)) q

Tactic:
exact hp₃ ⟨h₁, hq'⟩ h₂

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : PrimeSpectrum R
⊢ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal → p ∈ Set.range (comap f)

Tactic:
Ideal.comap_map_eq_self_iff_of_isPrime

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : PrimeSpectrum R
⊢ (∃ q, q.IsPrime ∧ Ideal.comap f q = p.asIdeal) → p ∈ Set.range (comap f)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr
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 R
p : Ideal A
⊢ p ∈ Ideal.under R ⁻¹' J.minimalPrimes → p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes

Tactic:
· intro hp
    refine ⟨⟨?_, Ideal.map_le_iff_le_comap.mpr hp.le⟩, ?_⟩
    · rw [IsLocalization.isPrime_iff_isPrime_disjoint S A, IsLocalization.disjoint_under_iff S]
      refine ⟨hp.isPrime, ?_⟩
      rintro rfl
      exact hp.isPrime.ne_top rfl
    · intro I hI e
      rw [← IsLocalization.map_under S A I, ← IsLocalization.map_under S A p]
      exact Ideal.map_mono (hp.2 ⟨hI.1.comap _, Ideal.map_le_iff_le_comap.mp hI.2⟩
        (Ideal.comap_mono e))

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]; exact fun _ _ ↦ .rfl

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]; exact fun _ _ ↦ .rfl

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]; exact fun _ _ ↦ .rfl

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]; exact fun _ _ ↦ .rfl

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B → ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

pp: case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ (∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U) → IsBasis B

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B → ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ (∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U) → IsBasis B
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst✝¹] t
⊢ IsCompact (⋂₀ s)

pp: α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
h : ∀ t ∈ s, IsOpen[inst✝¹] t
⊢ IsCompact (⋂₀ s)

Tactic:
· let a := { t ∈ s | IsOpen t }
    let b := { t ∈ s | IsClosed t }
    have heq : s = a ∪ b := subset_antisymm (by grind) (by grind)
    rw [heq, Set.sInter_union]
    simp only [not_forall] at h
    obtain ⟨t, ht, hno⟩ := h
    obtain (ha | ha) := a.eq_empty_or_nonempty
    · simp only [ha, Set.sInter_empty, Set.univ_inter]
      exact IsCompact.of_isClosed_subset (hc _ ht) (isClosed_sInter (by grind)) (by grind)
    · apply IsCompact.inter_right
      · apply this (hf.subset (by grind)) ha <;> grind
      · exact isClosed_sInter (by grind)

Goal state after:
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
h : ∀ t ∈ s, IsOpen[inst✝¹] t
⊢ IsCompact (⋂₀ s)
Module: Mathlib.Order.Ideal

Goal state before:
pp: case empty
P : Type u_2
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
⊢ ∅.sup f ∈ t ↔ ∀ i ∈ ∅, f i ∈ t

pp: case insert
P : Type u_2
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : s✝.sup f ∈ t ↔ ∀ i ∈ s✝, f i ∈ t
⊢ (insert a✝² s✝).sup f ∈ t ↔ ∀ i ∈ insert a✝² s✝, f i ∈ t

Tactic:
<;>

Goal state after:
case empty
P : Type u_2
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
⊢ ∅.sup f ∈ t ↔ ∀ i ∈ ∅, f i ∈ t

case insert
P : Type u_2
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : s✝.sup f ∈ t ↔ ∀ i ∈ s✝, f i ∈ t
⊢ (insert a✝² s✝).sup f ∈ t ↔ ∀ i ∈ insert a✝² s✝, f i ∈ t
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
h : Disjoint K L
⊢ ↑K ∩ ↑L ⊆ ∅

Tactic:
intro x ⟨hxK, hxL⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
h : Disjoint K L
x : α
hxK : x ∈ ↑K
hxL : x ∈ ↑L
⊢ x ∈ ∅
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Subsingleton (Compacts α) ↔ IsEmpty α

Tactic:
refine ⟨fun h => ?_, fun _ => inferInstance⟩
  contrapose! h
  infer_instance

Goal state after:
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₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
rw [PrespectralSpace.isTopologicalBasis.isOpen_iff] at hU₁ hU₂

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ 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₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact ((Finset.cons i s ih).sup t)

Tactic:
Finset.sup_cons

Goal state after:
case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact (t i ⊔ s.sup t)
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S U : Set α
h : IsGenericPoint x S
hU : IsOpen U
⊢ Disjoint S U ↔ ¬¬Disjoint S U

Tactic:
Classical.not_not

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S U : Set α
h : IsGenericPoint x S
hU : IsOpen U
⊢ Disjoint S U ↔ Disjoint S U
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: case empty
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
⊢ ↑(∅.sup f) = ⋃ i ∈ ∅, ↑(f i)

pp: case insert
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : ↑(s✝.sup f) = ⋃ i ∈ s✝, ↑(f i)
⊢ ↑((insert a✝² s✝).sup f) = ⋃ i ∈ insert a✝² s✝, ↑(f i)

Tactic:
<;>

Goal state after:
case empty
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
⊢ ↑(∅.sup f) = ⋃ i ∈ ∅, ↑(f i)

case insert
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : ↑(s✝.sup f) = ⋃ i ∈ s✝, ↑(f i)
⊢ ↑((insert a✝² s✝).sup f) = ⋃ i ∈ insert a✝² s✝, ↑(f i)
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑V
hW : IsClosed W
⊢ QuasiSober ↑(W ∩ V)

Tactic:
by
  rw [inter_comm]
  exact .inter_of_isClosed_of_quasiSober_left V hW

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
⊢ IsCompact (V₁ ∩ V₂)

Tactic:
convert!
      t.isCompact_biUnion fun i _ ↦
        h₂ i _ _ Set.inter_subset_left ((U i).2.inter ho₁) (h₁ i hc₁ ho₁) Set.inter_subset_left
          ((U i).2.inter ho₂) (h₁ i hc₂ ho₂)

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
⊢ V₁ ∩ V₂ = ⋃ i ∈ t, ↑(U i) ∩ V₁ ∩ (↑(U i) ∩ V₂)
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
f : AddAut (ZMod n)
x : ZMod n
⊢ x.cast • f 1 = f ↑x.cast

Tactic:
← map_zsmul,

Goal state after:
n : ℕ
f : AddAut (ZMod n)
x : ZMod n
⊢ f (x.cast • 1) = f ↑x.cast
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
x✝ : A
⊢ ((Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)).comp
        Algebra.TensorProduct.includeLeft)
      x✝

pp: case hb
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
x✝ : B
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g))).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
x✝ : A
⊢ ((Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)).comp
        Algebra.TensorProduct.includeLeft)
      x✝

case hb
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
x✝ : B
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g))).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
⊢ ⋂ i, ↑i ∈ Set.range zeroLocus

Tactic:
choose f hf using fun i : Zs => h i.prop

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
f : ↑Zs → Set R
hf : ∀ (i : ↑Zs), zeroLocus (f i) = ↑i
⊢ ⋂ i, ↑i ∈ Set.range zeroLocus
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
h✝ : b.factorization p ≤ a.factorization p
⊢ p ^ n * 1 = p ^ n

pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
h✝ : ¬b.factorization p ≤ a.factorization p
⊢ 1 * p ^ n = p ^ n

Tactic:
<;>

Goal state after:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
h✝ : b.factorization p ≤ a.factorization p
⊢ p ^ n * 1 = p ^ n

case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
h✝ : ¬b.factorization p ≤ a.factorization p
⊢ 1 * p ^ n = p ^ n
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ zeroLocus ↑x.asIdeal ⊆ {x} → x.asIdeal.IsMaximal

pp: case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ x.asIdeal.IsMaximal → zeroLocus ↑x.asIdeal ⊆ {x}

Tactic:
<;>

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ zeroLocus ↑x.asIdeal ⊆ {x} → x.asIdeal.IsMaximal

case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ x.asIdeal.IsMaximal → zeroLocus ↑x.asIdeal ⊆ {x}
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case e'_3
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ zeroLocus ↑(vanishingIdeal s) = closure s

pp: case e'_4
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ zeroLocus ↑(vanishingIdeal t) = closure t

Tactic:
<;>

Goal state after:
case e'_3
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ zeroLocus ↑(vanishingIdeal s) = closure s

case e'_4
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ zeroLocus ↑(vanishingIdeal t) = closure t
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_7
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        ((CommRingCat.ofHom (algebraMap S T) ≫
            pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A))) ≫
          ⋯.isoPushout.symm.hom))
      x✝ =
    (CommRingCat.Hom.hom
        ((Iso.refl (CommRingCat.of S)).hom ≫
          CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T))))
      x✝

Tactic:
<;>

Goal state after:
case refine_7
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        ((CommRingCat.ofHom (algebraMap S T) ≫
            pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A))) ≫
          ⋯.isoPushout.symm.hom))
      x✝ =
    (CommRingCat.Hom.hom
        ((Iso.refl (CommRingCat.of S)).hom ≫
          CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T))))
      x✝
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case zero
R : Type u
inst✝ : CommSemiring R
r : R
⊢ basicOpen r ≤ basicOpen (r ^ 0)

pp: case succ
R : Type u
inst✝ : CommSemiring R
r : R
n✝ : ℕ
⊢ basicOpen r ≤ basicOpen (r ^ (n✝ + 1))

Tactic:
<;>

Goal state after:
case zero
R : Type u
inst✝ : CommSemiring R
r : R
⊢ basicOpen r ≤ basicOpen (r ^ 0)

case succ
R : Type u
inst✝ : CommSemiring R
r : R
n✝ : ℕ
⊢ basicOpen r ≤ basicOpen (r ^ (n✝ + 1))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inl
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
x : (i : ι) → R i
hx : x i = 0
this : Pi.single i f * x = 0
h : Pi.single i f ∈ p.asIdeal
⊢ x ∈ p.asIdeal

pp: case inr
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
x : (i : ι) → R i
hx : x i = 0
this : Pi.single i f * x = 0
h : x ∈ p.asIdeal
⊢ x ∈ p.asIdeal

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
x : (i : ι) → R i
hx : x i = 0
this : Pi.single i f * x = 0
h : Pi.single i f ∈ p.asIdeal
⊢ x ∈ p.asIdeal

case inr
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
x : (i : ι) → R i
hx : x i = 0
this : Pi.single i f * x = 0
h : x ∈ p.asIdeal
⊢ x ∈ p.asIdeal
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ g' ∈ zpowers g

Tactic:
zpowers_eq_top_of_prime_card h hg,

Goal state after:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ g' ∈ ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
hH : IsCyclic G'
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
⊢ IsCyclic G

Tactic:
obtain ⟨x, hx⟩ := hH

Goal state after:
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 ↦ x ^ x_1
⊢ IsCyclic G
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
H : DenseRange (comap f)
p : Ideal S
hp : p.IsPrime
left✝ : ⊥ ≤ p
hI : Ideal.comap f p ∈ minimalPrimes R
this : Ideal.comap f p ∈ (RingHom.ker f).minimalPrimes
⊢ { asIdeal := Ideal.comap f p, isPrime := ⋯ } ∈ Set.range (comap f)

Tactic:
exact ⟨⟨p, hp⟩, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

pp: case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
<;>

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

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

Tactic:
<;>

Goal state after:
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