harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : a ∉ l₁) :
    (l₁ ++ l₂).erase a = (l₁ ++ l₂.erase a)

Proof state:
case a
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
h : ¬a ∈ l₁
⊢ ∀ (b : α), b ∈ l₁ → ¬(a == b) = true

Tactic:
intros b h' h''

Result:
case a
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
h : ¬a ∈ l₁
b : α
h' : b ∈ l₁
h'' : (a == b) = true
⊢ False

Proof state:
case a
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
b : α
h : ¬b ∈ l₁
h' : b ∈ l₁
h'' : (a == b) = true
⊢ False

Tactic:
exact h h'

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
h : ¬a ∈ l₁
b : α
h' : b ∈ l₁
h'' : (a == b) = true
⊢ False

Tactic:
rw [eq_of_beq h''] at h

Result:
case a
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
b : α
h : ¬b ∈ l₁
h' : b ∈ l₁
h'' : (a == b) = true
⊢ False

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
h : ¬a ∈ l₁
⊢ (l₁ ++ l₂).erase a = l₁ ++ l₂.erase a

Tactic:
rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_append_right]

Result:
case a
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
h : ¬a ∈ l₁
⊢ ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem preAleph_omega0 : preAleph ω = ℵ₀

Proof state:
⊢ preAleph ω = ℵ₀

Tactic:
rw [← card_preOmega, preOmega_omega0, card_omega0]

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
@[simp] lemma take_self_eq_iff (x : List α) {n : ℕ} : x = x.take n ↔ x.length ≤ n

Proof state:
α : Type u
x : List α
n : ℕ
⊢ x = take n x ↔ x.length ≤ n

Tactic:
rw [Eq.comm, take_eq_self_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprodComparison_inv_natural (f : A ⟶ A') (g : B ⟶ B') [IsIso (coprodComparison F A B)]
    [IsIso (coprodComparison F A' B')] :
    inv (coprodComparison F A B) ≫ coprod.map (F.map f) (F.map g) =
      F.map (coprod.map f g) ≫ inv (coprodComparison F A' B')

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁵ : HasBinaryCoproduct A B
inst✝⁴ : HasBinaryCoproduct A' B'
inst✝³ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝² : HasBinaryCoproduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst✝¹ : IsIso (coprodComparison F A B)
inst✝ : IsIso (coprodComparison F A' B')
⊢ inv (coprodComparison F A B) ≫ coprod.map (F.map f) (F.map g) =
    F.map (coprod.map f g) ≫ inv (coprodComparison F A' B')

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, coprodComparison_natural]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem subset_map_symm {t : Finset β} {f : α ≃ β} : s ⊆ t.map f.symm ↔ s.map f ⊆ t

Proof state:
case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ x ∈ map f.symm.toEmbedding t

Tactic:
simp only [mem_map_equiv]

Result:
case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ f.symm.symm x ∈ t

Proof state:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : f.symm x ∈ s
⊢ x ∈ t

Tactic:
simpa using h hx

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : x ∈ map f.toEmbedding s
⊢ x ∈ t

Tactic:
simp only [mem_map_equiv, Equiv.symm_symm] at hx

Result:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : f.symm x ∈ s
⊢ x ∈ t

Proof state:
case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ f.symm.symm x ∈ t

Tactic:
exact h (by simp [hx])

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ s ⊆ map f.symm.toEmbedding t ↔ map f.toEmbedding s ⊆ t

Tactic:
constructor <;> intro h x hx

Result:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : x ∈ map f.toEmbedding s
⊢ x ∈ t

case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ x ∈ map f.symm.toEmbedding t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ f.symm.symm x ∈ map f.toEmbedding s

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Order/Filter/CountableInter.lean
theorem EventuallyLE.countable_bInter {ι : Type*} {S : Set ι} (hS : S.Countable)
    {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) :
    ⋂ i ∈ S, s i ‹_› ≤ᶠ[l] ⋂ i ∈ S, t i ‹_›

Proof state:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h

Tactic:
simp only [biInter_eq_iInter]

Result:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯

Proof state:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable ↑S
⊢ ⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯

Tactic:
exact EventuallyLE.countable_iInter fun i => h i i.2

Result:
no goals

Proof state:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯

Tactic:
haveI := hS.toEncodable

Result:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
this : Encodable ↑S
⊢ ⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@[simp]
lemma toNNReal_neg_smul (r : ℝ≥0) (f : C(X, ℝ)₀) : (-(r • f)).toNNReal = r • (-f).toNNReal

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
⊢ (-(r • f)).toNNReal = r • (-f).toNNReal

Tactic:
rw [NNReal.smul_def, ← smul_neg, ← NNReal.smul_def, toNNReal_smul]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_pi : o.rotation π = LinearIsometryEquiv.neg ℝ

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
⊢ o.rotation ↑π = LinearIsometryEquiv.neg ℝ

Tactic:
ext x

Result:
case h
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ (o.rotation ↑π) x = (LinearIsometryEquiv.neg ℝ) x

Proof state:
case h
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ (o.rotation ↑π) x = (LinearIsometryEquiv.neg ℝ) x

Tactic:
simp [rotation]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem map_bijective_iff {f : α → β} : Bijective (map f) ↔ Bijective f

Proof state:
α : Type u
β : Type v
f : α → β
⊢ Bijective (map f) ↔ Bijective f

Tactic:
simp_rw [Function.Bijective, map_injective_iff, map_surjective_iff]

Result:
no goals
-- Mathlib/Data/Quot.lean
theorem Quotient.induction_on_pi {ι : Type*} {α : ι → Sort*} {s : ∀ i, Setoid (α i)}
    {p : (∀ i, Quotient (s i)) → Prop} (f : ∀ i, Quotient (s i))
    (h : ∀ a : ∀ i, α i, p fun i ↦ ⟦a i⟧) : p f

Proof state:
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i => ⟦a i⟧
⊢ p f

Tactic:
rw [← (funext fun i ↦ Quotient.out_eq (f i) : (fun i ↦ ⟦(f i).out⟧) = f)]

Result:
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i => ⟦a i⟧
⊢ p fun i => ⟦(f i).out⟧

Proof state:
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i => ⟦a i⟧
⊢ p fun i => ⟦(f i).out⟧

Tactic:
apply h

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem map_PInfty_f {D : Type*} [Category D] [Preadditive D] (G : C ⥤ D) [G.Additive]
    (X : SimplicialObject C) (n : ℕ) :
    (PInfty : K[((whiskering C D).obj G).obj X] ⟶ _).f n =
      G.map ((PInfty : AlternatingFaceMapComplex.obj X ⟶ _).f n)

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n = G.map (PInfty.f n)

Tactic:
simp only [PInfty_f, map_P]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem pow_zero_eq_zeta : pow 0 = ζ

Proof state:
⊢ pow 0 = ζ

Tactic:
ext n

Result:
case h
n : ℕ
⊢ (pow 0) n = ζ n

Proof state:
case h
n : ℕ
⊢ (pow 0) n = ζ n

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem frequently_nhdsWithin_iff {z : α} {s : Set α} {p : α → Prop} :
    (∃ᶠ x in 𝓝[s] z, p x) ↔ ∃ᶠ x in 𝓝 z, p x ∧ x ∈ s :=
  frequently_inf_principal.trans <| by simp only [and_comm]

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
z : α
s : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in 𝓝 z, x ∈ s ∧ p x) ↔ ∃ᶠ (x : α) in 𝓝 z, p x ∧ x ∈ s

Tactic:
simp only [and_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
lemma exists_nat_gt (x : α) : ∃ n : ℕ, x < n :=
  (exists_lt_nsmul zero_lt_one x).imp fun n hn ↦ by rwa [← nsmul_one]

Proof state:
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Archimedean α
x : α
n : ℕ
hn : x < n • 1
⊢ x < ↑n

Tactic:
rwa [← nsmul_one]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castPred_eq_iff_eq_castSucc (i : Fin (n + 1)) (hi : i ≠ last _) (j : Fin n) :
    castPred i hi = j ↔ i = castSucc j :=
  ⟨fun h => by rw [← h, castSucc_castPred], fun h => by simp_rw [h, castPred_castSucc]⟩

Proof state:
n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i = j.castSucc
⊢ i.castPred hi = j

Tactic:
simp_rw [h, castPred_castSucc]

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i.castPred hi = j
⊢ i = j.castSucc

Tactic:
rw [← h, castSucc_castPred]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
theorem charmatrix_apply_eq : charmatrix M i i = (X : R[X]) - C (M i i)

Proof state:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i : n
⊢ M.charmatrix i i = X - C (M i i)

Tactic:
simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply, map_apply,
  diagonal_apply_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma not_continuousAt_deriv_mul_log_zero :
    ¬ ContinuousAt (deriv (fun (x : ℝ) ↦ x * log x)) 0 :=
  not_continuousAt_of_tendsto tendsto_deriv_mul_log_nhdsWithin_zero nhdsWithin_le_nhds (by simp)

Proof state:
⊢ Disjoint (𝓝 (deriv (fun x => x * log x) 0)) Filter.atBot

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_one_div (x y : G) : x * (1 / y) = x / y

Proof state:
G : Type u_3
inst✝ : DivInvMonoid G
x y : G
⊢ x * (1 / y) = x / y

Tactic:
rw [div_eq_mul_inv, one_mul, div_eq_mul_inv]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem mem_normalizedFactors_eq_of_associated {a b c : α} (ha : a ∈ normalizedFactors c)
    (hb : b ∈ normalizedFactors c) (h : Associated a b) : a = b

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b c : α
ha : a ∈ normalizedFactors c
hb : b ∈ normalizedFactors c
h : a ~ᵤ b
⊢ a ∣ b ∧ b ∣ a

Tactic:
exact Associated.dvd_dvd h

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b c : α
ha : a ∈ normalizedFactors c
hb : b ∈ normalizedFactors c
h : a ~ᵤ b
⊢ a = b

Tactic:
rw [← normalize_normalized_factor a ha, ← normalize_normalized_factor b hb,
  normalize_eq_normalize_iff]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b c : α
ha : a ∈ normalizedFactors c
hb : b ∈ normalizedFactors c
h : a ~ᵤ b
⊢ a ∣ b ∧ b ∣ a
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem ker_quotQuotMk : RingHom.ker (quotQuotMk I J) = I ⊔ J

Proof state:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.ker (quotQuotMk I J) = I ⊔ J

Tactic:
rw [RingHom.ker_eq_comap_bot, quotQuotMk, ← comap_comap, ← RingHom.ker, mk_ker,
  comap_map_of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective, ← RingHom.ker,
  mk_ker, sup_comm]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
lemma prop_iff {X Y : C} (f : X ⟶ Y) :
    Φ.prop f ↔ Arrow.mk f = Φ.toSuccArrow X

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.toSuccArrow X ∈ Φ.prop.toSet

Tactic:
apply prop_toSucc

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
⊢ Arrow.mk f = Φ.toSuccArrow X → Φ.prop f

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.prop f

Proof state:
case mp.mk
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X✝ X Y : C
⊢ Arrow.mk (Φ.toSucc X✝) = Φ.toSuccArrow X✝

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
⊢ Φ.prop f ↔ Arrow.mk f = Φ.toSuccArrow X

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
⊢ Φ.prop f → Arrow.mk f = Φ.toSuccArrow X

case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
⊢ Arrow.mk f = Φ.toSuccArrow X → Φ.prop f

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
⊢ Φ.prop f → Arrow.mk f = Φ.toSuccArrow X

Tactic:
rintro ⟨_⟩

Result:
case mp.mk
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X✝ X Y : C
⊢ Arrow.mk (Φ.toSucc X✝) = Φ.toSuccArrow X✝

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.prop f

Tactic:
rw [← Φ.prop.arrow_mk_mem_toSet_iff, h]

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.toSuccArrow X ∈ Φ.prop.toSet
-- Mathlib/RingTheory/Trace/Quotient.lean
lemma IsLocalization.AtPrime.map_eq_maximalIdeal :
    p.map (algebraMap R Rₚ) = maximalIdeal Rₚ

Proof state:
case h.e'_3
R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_3
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ maximalIdeal Rₚ = Ideal.map (algebraMap R Rₚ) (Ideal.comap (algebraMap R Rₚ) (maximalIdeal Rₚ))

Tactic:
rw [map_comap p.primeCompl]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_3
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ Ideal.map (algebraMap R Rₚ) p = maximalIdeal Rₚ

Tactic:
convert congr_arg (Ideal.map (algebraMap R Rₚ))
  (IsLocalization.AtPrime.comap_maximalIdeal Rₚ p).symm

Result:
case h.e'_3
R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_3
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ maximalIdeal Rₚ = Ideal.map (algebraMap R Rₚ) (Ideal.comap (algebraMap R Rₚ) (maximalIdeal Rₚ))
-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem squashGCF_nth_of_lt {m : ℕ} (m_lt_n : m < n) :
    (squashGCF g (n + 1)).s.get? m = g.s.get? m

Proof state:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
⊢ (g.squashGCF (n + 1)).s.get? m = g.s.get? m

Tactic:
simp only [squashGCF, squashSeq_nth_of_lt m_lt_n, Nat.add_eq, add_zero]

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem not_mem_sigmaLift_of_ne_left (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α)
    (b : Sigma β) (x : Sigma γ) (h : a.1 ≠ x.1) : x ∉ sigmaLift f a b

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ ¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)

Tactic:
exact fun H => h H.fst

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ x ∉ sigmaLift f a b

Tactic:
rw [mem_sigmaLift]

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ ¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_map (f : α → β) (a : Vector α n) (i : Nat) (hi : i < n) :
    (a.map f)[i] = f a[i]

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
a : Vector α n
i : Nat
hi : i < n
⊢ (map f a)[i] = f a[i]

Tactic:
cases a

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (map f { toArray := toArray✝, size_toArray := size_toArray✝ })[i] =
    f { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (map f { toArray := toArray✝, size_toArray := size_toArray✝ })[i] =
    f { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
@[simp] lemma reverse_X_pow_mul (p : R[X]) (n : ℕ) : reverse (X ^ n * p) = reverse p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (X ^ n * p).reverse = p.reverse

Tactic:
rw [commute_X_pow p, reverse_mul_X_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_reverse {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
    l.reverse.mapFinIdx f = (l.mapFinIdx (fun i a h => f (n - 1 - i) a (by omega))).reverse

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : (i : Nat) → α → i < n → β
⊢ l.reverse.mapFinIdx f = (l.mapFinIdx fun i a h => f (n - 1 - i) a ⋯).reverse

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ { toArray := l, size_toArray := ⋯ }.reverse.mapFinIdx f =
    ({ toArray := l, size_toArray := ⋯ }.mapFinIdx fun i a h => f (l.size - 1 - i) a ⋯).reverse

Proof state:
case mk
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ { toArray := l, size_toArray := ⋯ }.reverse.mapFinIdx f =
    ({ toArray := l, size_toArray := ⋯ }.mapFinIdx fun i a h => f (l.size - 1 - i) a ⋯).reverse

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.63647
n : Nat
β : Type ?u.63669
l : Vector α n
f : (i : Nat) → α → i < n → β
i : Nat
a : α
h : i < n
⊢ n - 1 - i < n

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
    (Const.modify m k f).getKey? k = if k ∈ m then some k else none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey? k = if k ∈ m then some k else none

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey? k = if m.contains k = true then some k else none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey? k = if m.contains k = true then some k else none

Tactic:
simp_to_raw using Raw₀.Const.getKey?_modify_self

Result:
no goals
-- Mathlib/Topology/List.lean
theorem tendsto_insertIdx' {a : α} :
    ∀ {n : ℕ} {l : List α},
      Tendsto (fun p : α × List α => insertIdx n p.1 p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx n a l))
  | 0, _ => tendsto_cons
  | n + 1, [] => by simp
  | n + 1, a'::l => by
    have : 𝓝 a ×ˢ 𝓝 (a'::l) =
        (𝓝 a ×ˢ (𝓝 a' ×ˢ 𝓝 l)).map fun p : α × α × List α => (p.1, p.2.1::p.2.2)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ Prod.mk <$> 𝓝 a <*> (cons <$> 𝓝 a' <*> 𝓝 l) =
    (fun p => (p.1, p.2.1 :: p.2.2)) <$> (Prod.mk <$> 𝓝 a <*> (Prod.mk <$> 𝓝 a' <*> 𝓝 l))

Tactic:
simp [-Filter.map_def, Function.comp_def, functor_norm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto (fun p => insertIdx (n + 1) p.1 p.2) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 (insertIdx (n + 1) a (a' :: l)))

Tactic:
rw [this, tendsto_map'_iff]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto ((fun p => insertIdx (n + 1) p.1 p.2) ∘ fun p => (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
    (𝓝 (insertIdx (n + 1) a (a' :: l)))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
⊢ Tendsto (fun p => insertIdx (n + 1) p.1 p.2) (𝓝 a ×ˢ 𝓝 []) (𝓝 (insertIdx (n + 1) a []))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)

Tactic:
simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ Prod.mk <$> 𝓝 a <*> (cons <$> 𝓝 a' <*> 𝓝 l) =
    (fun p => (p.1, p.2.1 :: p.2.2)) <$> (Prod.mk <$> 𝓝 a <*> (Prod.mk <$> 𝓝 a' <*> 𝓝 l))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ Tendsto (fun p => insertIdx (n + 1) p.1 p.2) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 (insertIdx (n + 1) a (a' :: l)))

Tactic:
have : 𝓝 a ×ˢ 𝓝 (a'::l) =
    (𝓝 a ×ˢ (𝓝 a' ×ˢ 𝓝 l)).map fun p : α × α × List α => (p.1, p.2.1::p.2.2) := by
  simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]
  simp [-Filter.map_def, Function.comp_def, functor_norm]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto (fun p => insertIdx (n + 1) p.1 p.2) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 (insertIdx (n + 1) a (a' :: l)))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto ((fun p => insertIdx (n + 1) p.1 p.2) ∘ fun p => (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
    (𝓝 (insertIdx (n + 1) a (a' :: l)))

Tactic:
exact
  (tendsto_fst.comp tendsto_snd).cons
    ((@tendsto_insertIdx' _ n l).comp <| tendsto_fst.prod_mk <| tendsto_snd.comp tendsto_snd)

Result:
no goals