harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
    (x.sshiftRight n).msb = x.msb

Proof state:
w n : Nat
x : BitVec w
hw₀ : ¬w = 0
⊢ ¬w ≤ w - 1

Tactic:
omega

Result:
no goals

Proof state:
case neg
w n : Nat
x : BitVec w
hw₀ : ¬w = 0
h : n + (w - 1) < w
⊢ x.getLsbD (n + (w - 1)) = x.getLsbD (w - 1)

Tactic:
simp [show n = 0 by omega]

Result:
no goals

Proof state:
w n : Nat
x : BitVec w
⊢ (x.sshiftRight n).msb = x.msb

Tactic:
rw [msb_eq_getLsbD_last, getLsbD_sshiftRight, msb_eq_getLsbD_last]

Result:
w n : Nat
x : BitVec w
⊢ (!decide (w ≤ w - 1) && if n + (w - 1) < w then x.getLsbD (n + (w - 1)) else x.getLsbD (w - 1)) = x.getLsbD (w - 1)

Proof state:
w n : Nat
x : BitVec w
hw₀ : ¬w = 0
h : n + (w - 1) < w
⊢ n = 0

Tactic:
omega

Result:
no goals

Proof state:
case pos
w n : Nat
x : BitVec w
hw₀ : w = 0
⊢ (!decide (w ≤ w - 1) && if n + (w - 1) < w then x.getLsbD (n + (w - 1)) else x.getLsbD (w - 1)) = x.getLsbD (w - 1)

Tactic:
simp [hw₀]

Result:
no goals

Proof state:
w n : Nat
x : BitVec w
⊢ (!decide (w ≤ w - 1) && if n + (w - 1) < w then x.getLsbD (n + (w - 1)) else x.getLsbD (w - 1)) = x.getLsbD (w - 1)

Tactic:
by_cases hw₀ : w = 0

Result:
case pos
w n : Nat
x : BitVec w
hw₀ : w = 0
⊢ (!decide (w ≤ w - 1) && if n + (w - 1) < w then x.getLsbD (n + (w - 1)) else x.getLsbD (w - 1)) = x.getLsbD (w - 1)

case neg
w n : Nat
x : BitVec w
hw₀ : ¬w = 0
⊢ (!decide (w ≤ w - 1) && if n + (w - 1) < w then x.getLsbD (n + (w - 1)) else x.getLsbD (w - 1)) = x.getLsbD (w - 1)

Proof state:
case neg
w n : Nat
x : BitVec w
hw₀ : ¬w = 0
⊢ (!decide (w ≤ w - 1) && if n + (w - 1) < w then x.getLsbD (n + (w - 1)) else x.getLsbD (w - 1)) = x.getLsbD (w - 1)

Tactic:
simp only [show ¬(w ≤ w - 1) by omega, decide_false, Bool.not_false, Bool.true_and,
  ite_eq_right_iff]

Result:
case neg
w n : Nat
x : BitVec w
hw₀ : ¬w = 0
⊢ n + (w - 1) < w → x.getLsbD (n + (w - 1)) = x.getLsbD (w - 1)

Proof state:
case neg
w n : Nat
x : BitVec w
hw₀ : ¬w = 0
⊢ n + (w - 1) < w → x.getLsbD (n + (w - 1)) = x.getLsbD (w - 1)

Tactic:
intros h

Result:
case neg
w n : Nat
x : BitVec w
hw₀ : ¬w = 0
h : n + (w - 1) < w
⊢ x.getLsbD (n + (w - 1)) = x.getLsbD (w - 1)
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem associated_of_irreducible {a b : R} (ha : Irreducible a) (hb : Irreducible b) :
    Associated a b

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : maximalIdeal R = span {a}
hb : maximalIdeal R = span {b}
⊢ Associated a b

Tactic:
rw [← span_singleton_eq_span_singleton, ← ha, hb]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : Irreducible a
hb : Irreducible b
⊢ Associated a b

Tactic:
rw [irreducible_iff_uniformizer] at ha hb

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : maximalIdeal R = span {a}
hb : maximalIdeal R = span {b}
⊢ Associated a b
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_map_of_injective [CommSemiring S] (p : MvPolynomial σ R) {f : R →+* S}
    (hf : Injective f) : (map f p).degrees = p.degrees

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
hf : Injective ⇑f
⊢ ((map f) p).degrees = p.degrees

Tactic:
simp only [degrees, MvPolynomial.support_map_of_injective _ hf]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
lemma _root_.fderivWithin_continuousLinearEquiv_comp (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G))
    (hs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) s x =
      (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderivWithin 𝕜 f s x)

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
x : E
s : Set E
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun x => (↑L).comp (f x)) s x =
    (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderivWithin 𝕜 f s x)

Tactic:
change fderivWithin 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) s x = _

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
x : E
s : Set E
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) s x =
    (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderivWithin 𝕜 f s x)

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
x : E
s : Set E
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) s x =
    (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderivWithin 𝕜 f s x)

Tactic:
rw [ContinuousLinearEquiv.comp_fderivWithin _ hs]

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
@[simp] lemma mem_primeFactorsList' {n p} : p ∈ n.primeFactorsList ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0

Proof state:
n p : ℕ
⊢ p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
cases n <;> simp [mem_primeFactorsList, *]

Result:
no goals
-- Mathlib/CategoryTheory/Action/Concrete.lean
lemma toEndHom_trivial_of_mem [N.Normal] {n : G} (hn : n ∈ N) : toEndHom N n = 𝟙 (G ⧸ₐ N)

Proof state:
case h
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
n : G
hn : n ∈ N
⊢ ((toEndHom N) n).hom = (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))).hom

Tactic:
ext (x : G ⧸ N)

Result:
case h.h
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
n : G
hn : n ∈ N
x : G ⧸ N
⊢ ((toEndHom N) n).hom x = (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))).hom x

Proof state:
case h.h
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
n : G
hn : n ∈ N
x : G ⧸ N
⊢ ((toEndHom N) n).hom x = (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))).hom x

Tactic:
induction' x using Quotient.inductionOn with μ

Result:
case h.h.h
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
n : G
hn : n ∈ N
μ : G
⊢ ((toEndHom N) n).hom ⟦μ⟧ = (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))).hom ⟦μ⟧

Proof state:
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
n : G
hn : n ∈ N
⊢ (toEndHom N) n = 𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))

Tactic:
apply Action.hom_ext

Result:
case h
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
n : G
hn : n ∈ N
⊢ ((toEndHom N) n).hom = (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))).hom

Proof state:
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
n : G
hn : n ∈ N
μ : G
⊢ (μ * n⁻¹)⁻¹ * μ ∈ N

Tactic:
simpa

Result:
no goals

Proof state:
case h.h.h
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
n : G
hn : n ∈ N
μ : G
⊢ ((toEndHom N) n).hom ⟦μ⟧ = (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))).hom ⟦μ⟧

Tactic:
exact Quotient.sound ((QuotientGroup.leftRel_apply).mpr <| by simpa)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1))

Proof state:
n i : Nat
⊢ (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1))

Tactic:
simp [range_eq_range', erase_range']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.post_π (j : J) : limit.post F G ≫ limit.π (F ⋙ G) j = G.map (limit.π F j)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
j : J
⊢ (G.mapCone (cone F)).π.app j = G.map (π F j)

Tactic:
rfl

Result:
no goals

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
j : J
⊢ post F G ≫ π (F ⋙ G) j = G.map (π F j)

Tactic:
erw [IsLimit.fac]

Result:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
j : J
⊢ (G.mapCone (cone F)).π.app j = G.map (π F j)
-- Mathlib/Order/Antichain.lean
/-- The intersection of a chain and an antichain is subsingleton. -/
lemma inter_subsingleton_of_isChain_of_isAntichain (hs : IsChain r s) (ht : IsAntichain r t) :
    (s ∩ t).Subsingleton :=
  subsingleton_of_isChain_of_isAntichain (hs.mono (by simp)) (ht.subset (by simp))

Proof state:
α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsChain r s
ht : IsAntichain r t
⊢ s ∩ t ⊆ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsChain r s
ht : IsAntichain r t
⊢ s ∩ t ⊆ t

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/T0Sierpinski.lean
theorem productOfMemOpens_injective [T0Space X] : Function.Injective (productOfMemOpens X)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
⊢ Function.Injective ⇑(productOfMemOpens X)

Tactic:
intro x1 x2 h

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ x1 = x2

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ Inseparable x1 x2

Tactic:
rw [← IsInducing.inseparable_iff (productOfMemOpens_isInducing X), h]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ x1 = x2

Tactic:
apply Inseparable.eq

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ Inseparable x1 x2
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
@[simp]
lemma homMap_id  :
    Φ.homMap L₁ L₂ (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj (Φ.functor.obj X))

Proof state:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_10, u_2} C₁
inst✝⁴ : Category.{u_9, u_3} C₂
inst✝³ : Category.{u_11, u_5} D₁
inst✝² : Category.{u_8, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X : C₁
⊢ Φ.homMap L₁ L₂ (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj (Φ.functor.obj X))

Tactic:
simpa using Φ.homMap_map L₁ L₂ (𝟙 X)

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousOn_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} {s : Set (α × β)} :
    ContinuousOn f s ↔ ∀ a, ContinuousOn (f ⟨a, ·⟩) {b | (a, b) ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (a : α), ContinuousOn (fun x => f (a, x)) {b | (a, b) ∈ s}

Tactic:
simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_left]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ (∀ (a : α) (b : β), (a, b) ∈ s → ContinuousWithinAt (fun x => f (a, x)) {b | (a, b) ∈ s} b) ↔
    ∀ (a : α), ∀ x ∈ {b | (a, b) ∈ s}, ContinuousWithinAt (fun x => f (a, x)) {b | (a, b) ∈ s} x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ (∀ (a : α) (b : β), (a, b) ∈ s → ContinuousWithinAt (fun x => f (a, x)) {b | (a, b) ∈ s} b) ↔
    ∀ (a : α), ∀ x ∈ {b | (a, b) ∈ s}, ContinuousWithinAt (fun x => f (a, x)) {b | (a, b) ∈ s} x

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem zero_lt_orderTop_iff {x : HahnSeries Γ R} (hx : x ≠ 0) :
    0 < x.orderTop ↔ 0 < x.order

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : x ≠ 0
⊢ 0 < x.orderTop ↔ 0 < x.order

Tactic:
simp_all [orderTop_of_ne hx, order_of_ne hx]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem comp_liftAddHom [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P)
    (f : α → M →+ N) :
    g.comp ((liftAddHom (α := α) (M := M) (N := N)) f) =
      (liftAddHom (α := α) (M := M) (N := P)) fun a => g.comp (f a) :=
  liftAddHom.symm_apply_eq.1 <|
    funext fun a => by
      rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
⊢ liftAddHom.symm (g.comp (liftAddHom f)) a = g.comp (f a)

Tactic:
rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

Result:
no goals
-- Mathlib/RingTheory/Ideal/AssociatedPrime.lean
theorem IsAssociatedPrime.map_of_injective (h : IsAssociatedPrime I M) (hf : Function.Injective f) :
    IsAssociatedPrime I M'

Proof state:
case intro.h
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (ker (toSpanSingleton R M x)) M
r : R
⊢ r ∈ ker (toSpanSingleton R M x) ↔ r ∈ ker (toSpanSingleton R M' (f x))

Tactic:
simp_rw [mem_ker, toSpanSingleton_apply, ← map_smul, ← f.map_zero, hf.eq_iff]

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (ker (toSpanSingleton R M x)) M
⊢ IsAssociatedPrime (ker (toSpanSingleton R M x)) M'

Tactic:
refine ⟨h.1, ⟨f x, ?_⟩⟩

Result:
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (ker (toSpanSingleton R M x)) M
⊢ ker (toSpanSingleton R M x) = ker (toSpanSingleton R M' (f x))

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : IsAssociatedPrime I M
hf : Function.Injective ⇑f
⊢ IsAssociatedPrime I M'

Tactic:
obtain ⟨x, rfl⟩ := h.2

Result:
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (ker (toSpanSingleton R M x)) M
⊢ IsAssociatedPrime (ker (toSpanSingleton R M x)) M'

Proof state:
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (ker (toSpanSingleton R M x)) M
⊢ ker (toSpanSingleton R M x) = ker (toSpanSingleton R M' (f x))

Tactic:
ext r

Result:
case intro.h
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (ker (toSpanSingleton R M x)) M
r : R
⊢ r ∈ ker (toSpanSingleton R M x) ↔ r ∈ ker (toSpanSingleton R M' (f x))
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBasis.closure_inter_isBasis_closure (h : M.IsBasis (X ∩ I) X) (hI : M.Indep I) :
    M.IsBasis (M.closure X ∩ I) (M.closure X)

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
h : X ⊆ M.closure (X ∩ I)
hI : M.Indep I
⊢ M.closure X ⊆ M.closure (M.closure X ∩ I)

Tactic:
exact (M.closure_subset_closure_of_subset_closure h).trans (M.closure_subset_closure
  (inter_subset_inter_left _ (h.trans (M.closure_subset_closure inter_subset_left))))

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis (X ∩ I) X
hI : M.Indep I
⊢ M.IsBasis (M.closure X ∩ I) (M.closure X)

Tactic:
rw [hI.inter_isBasis_closure_iff_subset_closure_inter] at h ⊢

Result:
α : Type u_2
M : Matroid α
X I : Set α
h : X ⊆ M.closure (X ∩ I)
hI : M.Indep I
⊢ M.closure X ⊆ M.closure (M.closure X ∩ I)
-- Mathlib/CategoryTheory/Sites/Over.lean
lemma over_map_compatiblePreserving {X Y : C} (f : X ⟶ Y) :
    CompatiblePreserving (J.over Y) (Over.map f) where
  compatible {F Z _ x hx Y₁ Y₂ W f₁ f₂ g₁ g₂ hg₁ hg₂ h}

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
⊢ F.val.map f₁.op (x g₁ hg₁) = F.val.map f₂.op (x g₂ hg₂)

Tactic:
let g₂' : W' ⟶ Y₂ := Over.homMk f₂.left
  (by simpa using (Over.forget _).congr_map h.symm =≫ Z.hom)

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯
⊢ F.val.map f₁.op (x g₁ hg₁) = F.val.map f₂.op (x g₂ hg₂)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {i : Nat}, l[i]? = some a → l[i]! = a
  | _a::_, 0, _ => by
    rw [getElem!_pos] <;> simp_all
  | _::l, _+1, e => by
    simp at e
    simp_all [getElem!_of_getElem? (l := l) e]

Proof state:
α : Type u_1
a : α
inst✝ : Inhabited α
head✝ : α
l : List α
n✝ : Nat
e : l[n✝]? = some a
⊢ (head✝ :: l)[n✝ + 1]! = a

Tactic:
simp_all [getElem!_of_getElem? (l := l) e]

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : Inhabited α
_a : α
tail✝ : List α
x✝ : (_a :: tail✝)[0]? = some a
⊢ (_a :: tail✝)[0]! = a

Tactic:
rw [getElem!_pos] <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : Inhabited α
head✝ : α
l : List α
n✝ : Nat
e : (head✝ :: l)[n✝ + 1]? = some a
⊢ (head✝ :: l)[n✝ + 1]! = a

Tactic:
simp at e

Result:
α : Type u_1
a : α
inst✝ : Inhabited α
head✝ : α
l : List α
n✝ : Nat
e : l[n✝]? = some a
⊢ (head✝ :: l)[n✝ + 1]! = a
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem map_sin : map f (sin A) = sin A'

Proof state:
case h
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff A' n✝) ((map f) (sin A)) = (coeff A' n✝) (sin A')

Tactic:
simp [sin, apply_ite f]

Result:
no goals

Proof state:
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (sin A) = sin A'

Tactic:
ext

Result:
case h
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff A' n✝) ((map f) (sin A)) = (coeff A' n✝) (sin A')
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma RightFractionRel.unop {W : MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
    {z₁ z₂ : W.RightFraction X Y}
    (h : RightFractionRel z₁ z₂) : LeftFractionRel z₁.unop z₂.unop

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : W.RightFraction X Y
Z : Cᵒᵖ
t₁ : Z ⟶ z₁.X'
t₂ : Z ⟶ z₂.X'
hs : t₁ ≫ z₁.s = t₂ ≫ z₂.s
hf : t₁ ≫ z₁.f = t₂ ≫ z₂.f
ht : W (t₁ ≫ z₁.s)
⊢ LeftFractionRel z₁.unop z₂.unop

Tactic:
exact ⟨Opposite.unop Z, t₁.unop, t₂.unop, Quiver.Hom.op_inj hs,
  Quiver.Hom.op_inj hf, ht⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : W.RightFraction X Y
h : RightFractionRel z₁ z₂
⊢ LeftFractionRel z₁.unop z₂.unop

Tactic:
obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h

Result:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : W.RightFraction X Y
Z : Cᵒᵖ
t₁ : Z ⟶ z₁.X'
t₂ : Z ⟶ z₂.X'
hs : t₁ ≫ z₁.s = t₂ ≫ z₂.s
hf : t₁ ≫ z₁.f = t₂ ≫ z₂.f
ht : W (t₁ ≫ z₁.s)
⊢ LeftFractionRel z₁.unop z₂.unop
-- Mathlib/NumberTheory/FunctionField.lean
theorem inftyValuation.polynomial {p : Fq[X]} (hp : p ≠ 0) :
    inftyValuationDef Fq (algebraMap Fq[X] (RatFunc Fq) p) =
      Multiplicative.ofAdd (p.natDegree : ℤ)

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
hp' : (algebraMap Fq[X] (RatFunc Fq)) p ≠ 0
⊢ inftyValuationDef Fq ((algebraMap Fq[X] (RatFunc Fq)) p) = ↑(Multiplicative.ofAdd ↑p.natDegree)

Tactic:
rw [inftyValuationDef, if_neg hp', RatFunc.intDegree_polynomial]

Result:
no goals

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
⊢ (algebraMap Fq[X] (RatFunc Fq)) p ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
⊢ inftyValuationDef Fq ((algebraMap Fq[X] (RatFunc Fq)) p) = ↑(Multiplicative.ofAdd ↑p.natDegree)

Tactic:
have hp' : algebraMap Fq[X] (RatFunc Fq) p ≠ 0 := by simpa

Result:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
hp' : (algebraMap Fq[X] (RatFunc Fq)) p ≠ 0
⊢ inftyValuationDef Fq ((algebraMap Fq[X] (RatFunc Fq)) p) = ↑(Multiplicative.ofAdd ↑p.natDegree)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w

Proof state:
case succ
i w : Nat
⊢ (twoPow (w + 1) i).toNat = 2 ^ i % 2 ^ (w + 1)

Tactic:
simp only [twoPow, toNat_shiftLeft, toNat_ofNat]

Result:
case succ
i w : Nat
⊢ (1 % 2 ^ (w + 1)) <<< i % 2 ^ (w + 1) = 2 ^ i % 2 ^ (w + 1)

Proof state:
w i : Nat
⊢ (twoPow w i).toNat = 2 ^ i % 2 ^ w

Tactic:
rcases w with rfl | w

Result:
case zero
i : Nat
⊢ (twoPow 0 i).toNat = 2 ^ i % 2 ^ 0

case succ
i w : Nat
⊢ (twoPow (w + 1) i).toNat = 2 ^ i % 2 ^ (w + 1)

Proof state:
case zero
i : Nat
⊢ (twoPow 0 i).toNat = 2 ^ i % 2 ^ 0

Tactic:
simp [Nat.mod_one, toNat_of_zero_length]

Result:
no goals

Proof state:
case succ
i w : Nat
h1 : 1 < 2 ^ (w + 1)
⊢ (1 % 2 ^ (w + 1)) <<< i % 2 ^ (w + 1) = 2 ^ i % 2 ^ (w + 1)

Tactic:
rw [Nat.mod_eq_of_lt h1, Nat.shiftLeft_eq, Nat.one_mul]

Result:
no goals

Proof state:
case succ
i w : Nat
⊢ (1 % 2 ^ (w + 1)) <<< i % 2 ^ (w + 1) = 2 ^ i % 2 ^ (w + 1)

Tactic:
have h1 : 1 < 2 ^ (w + 1) := Nat.one_lt_two_pow (by omega)

Result:
case succ
i w : Nat
h1 : 1 < 2 ^ (w + 1)
⊢ (1 % 2 ^ (w + 1)) <<< i % 2 ^ (w + 1) = 2 ^ i % 2 ^ (w + 1)

Proof state:
i w : Nat
⊢ w + 1 ≠ 0

Tactic:
omega

Result:
no goals