mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M₂
inst✝ : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M ≃SL[σ₁₂] M₂
U : Submodule R₂ M₂
⊢ ↑(f.ofSubmodule' U) = (↑f ∘SL (Submodule.comap (↑↑f) U).subtypeL).codRestrict U ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow (Shrink.{w, u} C)
⊢ (Shrink.equivalence C).counit.app x✝.left ≫ x✝.hom ≫ (Shrink.equivalence C).counitInv.app x✝.right =
    eqToHom ⋯ ≫ x✝.hom ≫ eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv

Tactic:
obtain ⟨s, γ, δ, h₁, h₂⟩ := IsFiltered.bowtie
    (IsFiltered.leftToMax i₀ j) β (IsFiltered.rightToMax i₀ j) α

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X✝ Y : C
e : X✝ ≅ Y
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X : (isCardinalPresentable C κ).FullSubcategory
⊢ IsCardinalPresentable ((isCardinalPresentable C κ).ι.obj X) κ

Tactic:
by
  dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
κ : Cardinal.{w}
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)
h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
ι : Type w
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
l : J
hl : ∀ (i : ι), Nonempty (k i ⟶ l)
a : (i : ι) → k i ⟶ l := fun i ↦ ⋯.some
m : J
b : l ⟶ m
c : j ⟶ m
hm : ∀ (i : ι), (f i ≫ a i) ≫ b = c
⊢ ∀ (i : ι), f i ≫ (fun i ↦ a i ≫ b) i = c

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)
h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
l✝ : ι → J
p : (i : ι) → k ⟶ l✝ i
hp : ∀ (i : ι), f₁ i ≫ p i = f₂ i ≫ p i
l : J
a : (i : ι) → l✝ i ⟶ l
b : k ⟶ l
h : ∀ (i : ι), p i ≫ a i = b
i : ι
⊢ f₁ i ≫ b = f₂ i ≫ b

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N ⊗[R] ((i : ι) → M i)
⊢ (piRight R S N M) x = (piRightHom R S N M) x

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N ⊗[R] (ι → R)
⊢ (piScalarRight R S N ι) x = (piScalarRightHom R S N ι) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_3
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : ↑P
⊢ (ConcreteCategory.hom (g' ≫ c.ι.app i)) x = (ConcreteCategory.hom (g' ≫ c.ι.app i)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case h₀
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.fst = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯) ≫ c.fst

pp: case h₁
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.snd = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯) ≫ c.snd

Tactic:
· simpa using! congr(($e₁).left)

Goal state after:
case h₁
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m ≫ c.snd = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯) ≫ c.snd
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ Hom.left f.hom ≫ Hom.left (Y✝.π.app { as := j }) = Hom.left (f.hom ≫ Y✝.π.app { as := j })

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x✝ : Fintype J
⊢ (commaObj (Functor.fromPUnit R) (𝟭 CommRingCat)
        (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q)).IsClosedUnderLimitsOfShape
    (Discrete J)

Tactic:
have := hQp.isClosedUnderLimitsOfShape hQi R

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x✝ : Fintype J
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.IsClosedUnderFiniteProducts
⊢ (commaObj (Functor.fromPUnit R) (𝟭 CommRingCat)
        (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q)).IsClosedUnderLimitsOfShape
    (Discrete J)
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ (commaObj (Functor.fromPUnit R) (𝟭 CommRingCat)
        (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q)).IsClosedUnderLimitsOfShape
    WalkingParallelPair

Tactic:
exact hQe.isClosedUnderLimitsOfShape hQi _

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
x : ↑S
⊢ ((Hom.hom (Under.Hom.right h')).comp Algebra.TensorProduct.includeLeftRingHom) x =
    (((Hom.hom
                (Under.Hom.right
                  ((toAlgHom ((R.tensorProd S).map f)).equalizer (toAlgHom ((R.tensorProd S).map g))).val.toUnder)).comp
            (Hom.hom
              (Under.Hom.right (AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
                ofHom
                  (RingHom.id
                    ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                        (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g))))))).comp
        Algebra.TensorProduct.includeLeftRingHom)
      x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: case h₂
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
x : ↑(R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))).right
⊢ ((Hom.hom (Under.Hom.right h')).comp Algebra.TensorProduct.includeRight.toRingHom) x =
    (((Hom.hom
                (Under.Hom.right
                  ((toAlgHom ((R.tensorProd S).map f)).equalizer (toAlgHom ((R.tensorProd S).map g))).val.toUnder)).comp
            (Hom.hom
              (Under.Hom.right (AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
                ofHom
                  (RingHom.id
                    ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                        (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g))))))).comp
        Algebra.TensorProduct.includeRight.toRingHom)
      x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
heq :
  (Under.equalizerForkIsLimit ((R.tensorProd S).map f) ((R.tensorProd S).map g)).lift (Fork.ofι h' w') =
    (AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
      CategoryTheory.Under.homMk
        (ofHom
          (RingHom.id
            ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g)))))
        ⋯
⊢ Function.Bijective
      ⇑(ConcreteCategory.hom
          ((CategoryTheory.Under.forget S).map
            ((AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
              CategoryTheory.Under.homMk
                (ofHom
                  (RingHom.id
                    ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                        (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g)))))
                ⋯))) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))

Tactic:
rfl

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

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
⊢ ↑((tensorEqualizerAux S T f g) 0) = (Algebra.TensorProduct.map (AlgHom.id S T) (f.equalizer g).val) 0

Tactic:
rfl

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

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x✝ : T
y✝ : ↥(f.equalizer g)
⊢ ↑((tensorEqualizerAux S T f g) (x✝ ⊗ₜ[R] y✝)) =
    (Algebra.TensorProduct.map (AlgHom.id S T) (f.equalizer g).val) (x✝ ⊗ₜ[R] y✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
⊢ q = 0 ∨ IsPrimePow q

Tactic:
apply or_iff_not_imp_left.2

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
⊢ ¬q = 0 → IsPrimePow q
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
g : ↑a ∈ nonunits R
⊢ False

Tactic:
← IsLocalRing.mem_maximalIdeal

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
g : ↑a ∈ IsLocalRing.maximalIdeal R
⊢ False
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : Subalgebra K L
inv_mem : ∀ x ∈ S, x⁻¹ ∈ S
x✝ : L
⊢ x✝ ∈ (S.toIntermediateField inv_mem).toSubalgebra ↔ x✝ ∈ S

Tactic:
rfl

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x✝ : L
⊢ x✝ ∈ S.toIntermediateField ⋯ ↔ x✝ ∈ S

Tactic:
rfl

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : Subalgebra K L
hS : IsField ↥S
x✝ : L
⊢ x✝ ∈ (S.toIntermediateField' hS).toSubalgebra ↔ x✝ ∈ S

Tactic:
rfl

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x✝ : L
⊢ x✝ ∈ S.toIntermediateField' ⋯ ↔ x✝ ∈ S

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ (∀ (x : ℕ), ↑x ∈ I → ↑x = 0) ↔ Ideal.comap (Nat.castRingHom R) I ≤ Ideal.comap (Nat.castRingHom R) ⊥

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑(Rat.num 0) /ₚ ↑(Rat.pnatDen 0) = 0

Tactic:
by simp [divp]

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
⊢ Nonempty (Algebra ℚ R) → ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

pp: case mpr
R : Type u_1
inst✝ : CommRing R
⊢ (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) → Nonempty (Algebra ℚ R)

Tactic:
· intro h_alg
    have h_alg' : Algebra ℚ R := h_alg.some
    apply of_algebraRat

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
⊢ (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) → Nonempty (Algebra ℚ R)
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case mp.refine_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + k % z) • p = (z * (k / z) + k % z) • p

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ (∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p) ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
z : ℤ
hz : z ≠ 0
⊢ z • ψ = z • θ ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑z))

Tactic:
induction ψ using Quotient.inductionOn

Goal state after:
case h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
θ : R ⧸ AddSubgroup.zmultiples p
z : ℤ
hz : z ≠ 0
a✝ : R
⊢ z • ⟦a✝⟧ = z • θ ↔ ∃ k, ⟦a✝⟧ = θ + ↑(↑k • (p / ↑z))
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ (∃ k, ψ = θ + ↑(↑k • (p / ↑n))) ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
s : Seq α
⊢ none = Prod.fst <$> (fun a' ↦ (a', s.tail)) <$> none

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
s : Seq α
val✝ : α
⊢ some val✝ = Prod.fst <$> (fun a' ↦ (a', s.tail)) <$> some val✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : (Corec.f f none).fst = none
⊢ (Corec.f f (Corec.f f none).snd).fst = none

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.some.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h₁ : f b = none
h :
  (match none with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match none with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : f b = none
⊢ Option.map (fun a' ↦ (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match none with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
s : Stream' α
⊢ (s.head :: s.tail) 0 = s 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ (s.head :: s.tail) (n✝ + 1) = s (n✝ + 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n m : ℕ
s : Stream' α
⊢ (drop m s).get n = s.get (n + m)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mk
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s' : Seq α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
r✝ : R ⟨val✝, property✝⟩ s'
this : head ⟨val✝, property✝⟩ = s'.head ∧ R (tail ⟨val✝, property✝⟩) s'.tail
r : R (tail ⟨val✝, property✝⟩) s'.tail
⊢ ↑(tail ⟨val✝, property✝⟩) = (↑⟨val✝, property✝⟩).tail

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mk
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s : Seq α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
r✝ : R s ⟨val✝, property✝⟩
this : s.head = head ⟨val✝, property✝⟩ ∧ R s.tail (tail ⟨val✝, property✝⟩)
r : R s.tail (tail ⟨val✝, property✝⟩)
⊢ ↑(tail ⟨val✝, property✝⟩) = (↑⟨val✝, property✝⟩).tail

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case nil.nil.left
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ nil.head = nil.head

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
⊢ (f (a :: s).head :: map f (a :: s).tail).head :: (f (a :: s).head :: map f (a :: s).tail).tail = f a :: map f s

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ (zip f s₁ s₂).head :: (zip f s₁ s₂).tail = f s₁.head s₂.head :: zip f s₁.tail s₂.tail

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
a : α
⊢ (const a).get 0 = (a :: const a).get 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
a : α
n✝ : ℕ
⊢ (const a).get (n✝ + 1) = (a :: const a).get (n✝ + 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
⊢ motive' s₁ s₂

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
f : α → α
a : α
⊢ (iterate f a).get (0 + 1) = (iterate f (f a)).get 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
f : α → α
a : α
⊢ (iterate f a).head :: iterate f (f a) = a :: iterate f (f a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
f : α → α
a : α
⊢ iterate f a = a :: iterate f (f a)

Tactic:
by
  rw [← Stream'.eta (iterate f a)]
  rw [tail_iterate]; rfl

Goal state after: