harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma stabilizer_image_coe_quotient : stabilizer Q (q '' s) = ⊥

Proof state:
case h
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G ⧸ stabilizer G s
⊢ a ∈ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) ↔ a ∈ ⊥

Tactic:
induction' a using QuotientGroup.induction_on with a

Result:
case h.H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
⊢ ↑a ∈ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) ↔ ↑a ∈ ⊥

Proof state:
G : Type u_1
inst✝ : CommGroup G
s : Set G
⊢ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) = ⊥

Tactic:
ext a

Result:
case h
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G ⧸ stabilizer G s
⊢ a ∈ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) ↔ a ∈ ⊥

Proof state:
case h.H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
⊢ ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' s ↔ a • s = s

Tactic:
rw [this]

Result:
case h.H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
⊢ QuotientGroup.mk '' (a • s) = QuotientGroup.mk '' s ↔ a • s = s

Proof state:
case h.H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
h : QuotientGroup.mk '' (a • s) = QuotientGroup.mk '' s
⊢ a • s = s

Tactic:
rwa [QuotientGroup.image_coe_inj, mul_smul_comm, stabilizer_mul_self] at h

Result:
no goals

Proof state:
case h.H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
⊢ ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' s ↔ a • s = s

Tactic:
have : q a • q '' s = q '' (a • s) :=
  (image_smul_distrib (QuotientGroup.mk' <| stabilizer G s) _ _).symm

Result:
case h.H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
⊢ ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' s ↔ a • s = s

Proof state:
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
h : a • s = s
⊢ QuotientGroup.mk '' (a • s) = QuotientGroup.mk '' s

Tactic:
rw [h]

Result:
no goals

Proof state:
case h.H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
⊢ QuotientGroup.mk '' (a • s) = QuotientGroup.mk '' s ↔ a • s = s

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩

Result:
case h.H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
h : QuotientGroup.mk '' (a • s) = QuotientGroup.mk '' s
⊢ a • s = s

Proof state:
case h.H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
⊢ ↑a ∈ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) ↔ ↑a ∈ ⊥

Tactic:
simp only [mem_stabilizer_iff, Subgroup.mem_bot, QuotientGroup.eq_one_iff]

Result:
case h.H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
⊢ ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' s ↔ a • s = s
-- Mathlib/Analysis/Normed/Lp/LpEquiv.lean
theorem Memℓp.all (f : ∀ i, E i) : Memℓp f p

Proof state:
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f p

Tactic:
rcases p.trichotomy with (rfl | rfl | _h)

Result:
case inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f 0

case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f ⊤

case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
⊢ Memℓp f p

Proof state:
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f ⊤

Tactic:
exact memℓp_infty_iff.mpr (Set.Finite.bddAbove (Set.range fun i : α ↦ ‖f i‖).toFinite)

Result:
no goals

Proof state:
case inr.inr.intro
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
val✝ : Fintype α
⊢ Memℓp f p

Tactic:
exact memℓp_gen ⟨Finset.univ.sum _, hasSum_fintype _⟩

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
⊢ Memℓp f p

Tactic:
cases nonempty_fintype α

Result:
case inr.inr.intro
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
val✝ : Fintype α
⊢ Memℓp f p

Proof state:
case inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f 0

Tactic:
exact memℓp_zero_iff.mpr { i : α | f i ≠ 0 }.toFinite

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem pi_subset_pi_iff : pi s t₁ ⊆ pi s t₂ ↔ (∀ i ∈ s, t₁ i ⊆ t₂ i) ∨ pi s t₁ = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i

Tactic:
simpa only [eval_image_pi hi hne, eval_image_pi hi (hne.mono h)] using
  image_subset (fun f : ∀ i, α i => f i) h

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
⊢ (s.pi t₁).Nonempty → ∀ i ∈ s, t₁ i ⊆ t₂ i

Tactic:
intro hne i hi

Result:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ s.pi t₁ ⊆ s.pi t₂ ↔ (∀ i ∈ s, t₁ i ⊆ t₂ i) ∨ s.pi t₁ = ∅

Tactic:
refine
  ⟨fun h => or_iff_not_imp_right.2 ?_, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩

Result:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
⊢ ¬s.pi t₁ = ∅ → ∀ i ∈ s, t₁ i ⊆ t₂ i

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
⊢ ¬s.pi t₁ = ∅ → ∀ i ∈ s, t₁ i ⊆ t₂ i

Tactic:
rw [← Ne, ← nonempty_iff_ne_empty]

Result:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
⊢ (s.pi t₁).Nonempty → ∀ i ∈ s, t₁ i ⊆ t₂ i
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem differentiableWithinAt_insert {y : E} :
    DifferentiableWithinAt 𝕜 f (insert y s) x ↔ DifferentiableWithinAt 𝕜 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
f : E → F
x : E
s : Set E
y : E
⊢ DifferentiableWithinAt 𝕜 f (insert y s) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
rcases eq_or_ne x y with (rfl | h)

Result:
case inl
𝕜 : 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
f : E → F
x : E
s : Set E
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x ↔ DifferentiableWithinAt 𝕜 f s x

case inr
𝕜 : 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
f : E → F
x : E
s : Set E
y : E
h : x ≠ y
⊢ DifferentiableWithinAt 𝕜 f (insert y s) x ↔ DifferentiableWithinAt 𝕜 f s x

Proof state:
case inr.hst
𝕜 : 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
f : E → F
x : E
s : Set E
y : E
h : x ≠ y
⊢ 𝓝[insert y s] x = 𝓝[s] x

Tactic:
exact nhdsWithin_insert_of_ne h

Result:
no goals

Proof state:
case inl
𝕜 : 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
f : E → F
x : E
s : Set E
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
exact differentiableWithinAt_insert_self

Result:
no goals

Proof state:
case inr
𝕜 : 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
f : E → F
x : E
s : Set E
y : E
h : x ≠ y
⊢ DifferentiableWithinAt 𝕜 f (insert y s) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
apply differentiableWithinAt_congr_nhds

Result:
case inr.hst
𝕜 : 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
f : E → F
x : E
s : Set E
y : E
h : x ≠ y
⊢ 𝓝[insert y s] x = 𝓝[s] x
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem hsymmPart_zero : hsymmPart σ R (.indiscrete 0) = 1

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ hsymmPart σ R (Nat.Partition.indiscrete 0) = 1

Tactic:
simp [hsymmPart]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
theorem deriv_arcsin : deriv arcsin = fun x => 1 / √(1 - x ^ 2)

Proof state:
case neg
x : ℝ
h : x = -1 ∨ x = 1
⊢ 0 = 1 / √(1 - x ^ 2)

Tactic:
rcases h with (rfl | rfl) <;> simp

Result:
no goals

Proof state:
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Tactic:
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]

Result:
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ 0 = 1 / √(1 - x ^ 2)

Proof state:
case h
x : ℝ
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Tactic:
by_cases h : x ≠ -1 ∧ x ≠ 1

Result:
case pos
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Proof state:
⊢ deriv arcsin = fun x => 1 / √(1 - x ^ 2)

Tactic:
funext x

Result:
case h
x : ℝ
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Proof state:
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ 0 = 1 / √(1 - x ^ 2)

Tactic:
simp only [not_and_or, Ne, Classical.not_not] at h

Result:
case neg
x : ℝ
h : x = -1 ∨ x = 1
⊢ 0 = 1 / √(1 - x ^ 2)

Proof state:
case pos
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Tactic:
exact (hasDerivAt_arcsin h.1 h.2).deriv

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_alter_self (h : m.1.WF) {k : α} {f : Option β → Option β}
    {hc : (Const.alter m k f).contains k} :
    haveI h' : (f (Const.get? m k)).isSome

Proof state:
α : Type u
β✝ : α → Type v
m✝ : Raw₀ α β✝
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : Option β → Option β
hc : (alter m k f).contains k = true
⊢ (f (get? m k)).isSome = true

Tactic:
rwa [contains_alter _ h, BEq.refl] at hc

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : Option β → Option β
hc : (alter m k f).contains k = true
⊢ get (alter m k f) k hc = (f (get? m k)).get ⋯

Tactic:
simp_to_model [Const.alter] using List.Const.getValue_alterKey_self

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
theorem toMatrix_mul_apply [Fintype m] [DecidableEq m] [Semiring α] (f : l ≃. m) (M : Matrix m n α)
    (i j) : (f.toMatrix * M :) i j = Option.casesOn (f i) 0 fun fi => M fi j

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
⊢ (f.toMatrix * M) i j = Option.casesOn (f i) 0 fun fi => M fi j

Tactic:
dsimp [toMatrix, Matrix.mul_apply]

Result:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
⊢ ∑ j_1 : m, (if j_1 ∈ f i then 1 else 0) * M j_1 j = Option.rec 0 (fun val => M val j) (f i)

Proof state:
case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : f i = some fi
⊢ ∑ j_1 : m, (if j_1 ∈ some fi then 1 else 0) * M j_1 j = Option.rec 0 (fun val => M val j) (some fi)

Tactic:
rw [Finset.sum_eq_single fi] <;> simp +contextual [h, eq_comm]

Result:
no goals

Proof state:
case none
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
h : f i = none
⊢ ∑ j_1 : m, (if j_1 ∈ none then 1 else 0) * M j_1 j = Option.rec 0 (fun val => M val j) none

Tactic:
simp [h]

Result:
no goals

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
⊢ ∑ j_1 : m, (if j_1 ∈ f i then 1 else 0) * M j_1 j = Option.rec 0 (fun val => M val j) (f i)

Tactic:
rcases h : f i with - | fi

Result:
case none
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
h : f i = none
⊢ ∑ j_1 : m, (if j_1 ∈ none then 1 else 0) * M j_1 j = Option.rec 0 (fun val => M val j) none

case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : f i = some fi
⊢ ∑ j_1 : m, (if j_1 ∈ some fi then 1 else 0) * M j_1 j = Option.rec 0 (fun val => M val j) (some fi)
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
lemma PullbackCone.isIso_fst_of_mono_of_isLimit {t : PullbackCone f f} (ht : IsLimit t) :
    IsIso t.fst

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ ≫ t.fst = 𝟙 X

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
simp

Result:
no goals

Proof state:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.snd = 𝟙 t.pt ≫ t.snd

Tactic:
simp [fst_eq_snd_of_mono_eq]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsIso t.fst

Tactic:
refine ⟨⟨PullbackCone.IsLimit.lift ht (𝟙 _) (𝟙 _) (by simp), ?_, by simp⟩⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ = 𝟙 t.pt

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ = 𝟙 t.pt

Tactic:
apply PullbackCone.IsLimit.hom_ext ht

Result:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.fst = 𝟙 t.pt ≫ t.fst

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.snd = 𝟙 t.pt ≫ t.snd

Proof state:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.fst = 𝟙 t.pt ≫ t.fst

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem newton_seq_dist_to_a :
    ∀ n : ℕ, 0 < n → ‖newton_seq n - a‖ = ‖F.eval a‖ / ‖F.derivative.eval a‖
  | 1, _h => by simp [sub_eq_add_neg, add_assoc, newton_seq_gen, newton_seq_aux, ih_n]
  | k + 2, _h =>
    have hlt : ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖

Tactic:
rw [newton_seq_dist_to_a (k + 1) (succ_pos _)]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
hlt : ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖
hne' : ‖newton_seq (k + 2) - newton_seq (k + 1)‖ ≠ ‖newton_seq (k + 1) - a‖
⊢ ‖newton_seq (k + 2) - a‖ = ‖newton_seq (k + 2) - newton_seq (k + 1) + (newton_seq (k + 1) - a)‖

Tactic:
rw [← sub_add_sub_cancel]

Result:
no goals

Proof state:
case hnsol
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ Polynomial.eval a F ≠ 0

Tactic:
assumption

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
apply newton_seq_succ_dist_weak

Result:
case hnsol
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ Polynomial.eval a F ≠ 0

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
_h : 0 < 1
⊢ ‖newton_seq 1 - a‖ = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
simp [sub_eq_add_neg, add_assoc, newton_seq_gen, newton_seq_aux, ih_n]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
/-- A tensor product of symmetric bilinear forms is symmetric. -/
lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂}
    (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm

Proof state:
case a.h.h.a.h.h
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
x₁ : M₁
x₂ : M₂
y₁ : M₁
y₂ : M₂
⊢ ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (B₁.tmul B₂)) x₁) x₂)) y₁) y₂ =
    ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (LinearMap.flip (B₁.tmul B₂))) x₁) x₂)) y₁) y₂

Tactic:
exact congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁)

Result:
no goals

Proof state:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ IsSymm (B₁.tmul B₂)

Tactic:
rw [LinearMap.isSymm_iff_eq_flip]

Result:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ B₁.tmul B₂ = LinearMap.flip (B₁.tmul B₂)

Proof state:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ B₁.tmul B₂ = LinearMap.flip (B₁.tmul B₂)

Tactic:
ext x₁ x₂ y₁ y₂

Result:
case a.h.h.a.h.h
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
x₁ : M₁
x₂ : M₂
y₁ : M₁
y₂ : M₂
⊢ ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (B₁.tmul B₂)) x₁) x₂)) y₁) y₂ =
    ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (LinearMap.flip (B₁.tmul B₂))) x₁) x₂)) y₁) y₂
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_mk_eq_product [DecidableEq α] [DecidableEq β] (s : Finset α) (t : Finset β) :
    image₂ Prod.mk s t = s ×ˢ t

Proof state:
α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset β
⊢ image₂ Prod.mk s t = s ×ˢ t

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset β
a✝ : α × β
⊢ a✝ ∈ image₂ Prod.mk s t ↔ a✝ ∈ s ×ˢ t

Proof state:
case h
α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset β
a✝ : α × β
⊢ a✝ ∈ image₂ Prod.mk s t ↔ a✝ ∈ s ×ˢ t

Tactic:
simp [Prod.ext_iff]

Result:
no goals
-- Mathlib/Data/Multiset/DershowitzManna.lean
private lemma isDershowitzMannaLT_of_transGen_oneStep (hMN : TransGen OneStep M N) :
    IsDershowitzMannaLT M N :=
  hMN.trans_induction_on (by rintro _ _ ⟨X, Y, a, rfl, rfl, hYa⟩; exact ⟨X, Y, {a}, by simpa⟩)
    fun  _ _ ↦ .trans

Proof state:
α : Type u_1
inst✝ : Preorder α
M N : Multiset α
hMN : TransGen Multiset.OneStep M N
X Y : Multiset α
a : α
hYa : ∀ y ∈ Y, y < a
⊢ {a} ≠ ∅ ∧ X + Y = X + Y ∧ X + {a} = X + {a} ∧ ∀ y ∈ Y, ∃ z ∈ {a}, y < z

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
M N : Multiset α
hMN : TransGen Multiset.OneStep M N
⊢ ∀ {a b : Multiset α}, Multiset.OneStep a b → a.IsDershowitzMannaLT b

Tactic:
rintro _ _ ⟨X, Y, a, rfl, rfl, hYa⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
M N : Multiset α
hMN : TransGen Multiset.OneStep M N
X Y : Multiset α
a : α
hYa : ∀ y ∈ Y, y < a
⊢ (X + Y).IsDershowitzMannaLT (X + {a})

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
M N : Multiset α
hMN : TransGen Multiset.OneStep M N
X Y : Multiset α
a : α
hYa : ∀ y ∈ Y, y < a
⊢ (X + Y).IsDershowitzMannaLT (X + {a})

Tactic:
exact ⟨X, Y, {a}, by simpa⟩

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem norm_withSeminorms (𝕜 E) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
    WithSeminorms fun _ : Fin 1 => normSeminorm 𝕜 E

Proof state:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ 𝓝 0 = 𝓝 0

Tactic:
refine Filter.HasBasis.eq_of_same_basis Metric.nhds_basis_ball ?_

Result:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)