harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : E →ₐ[F] K) (s : ι → IntermediateField F E) :
    (iInf s).map f = ⨅ i, (s i).map f

Proof state:
F : Type u_1
inst✝⁵ : Field F
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
ι : Sort u_4
inst✝ : Nonempty ι
f : E →ₐ[F] K
s : ι → IntermediateField F E
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Result:
case a
F : Type u_1
inst✝⁵ : Field F
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
ι : Sort u_4
inst✝ : Nonempty ι
f : E →ₐ[F] K
s : ι → IntermediateField F E
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Proof state:
case a
F : Type u_1
inst✝⁵ : Field F
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
ι : Sort u_4
inst✝ : Nonempty ι
f : E →ₐ[F] K
s : ι → IntermediateField F E
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coe ∘ s)

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem exists_nontrivial_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) :
    ∃ a : Solution₁ d, a ≠ 1 ∧ a ≠ -1

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
⊢ ∃ a, a ≠ 1 ∧ a ≠ -1

Tactic:
obtain ⟨x, y, prop, hy⟩ := exists_of_not_isSquare h₀ hd

Result:
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ ∃ a, a ≠ 1 ∧ a ≠ -1

Proof state:
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ ∃ a, a ≠ 1 ∧ a ≠ -1

Tactic:
refine ⟨mk x y prop, fun H => ?_, fun H => ?_⟩ <;> apply_fun Solution₁.y at H <;>
  simp [hy] at H

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma exact₁ (S : ComposableArrows C 1) : S.Exact where
  toIsComplex := S.isComplex₁
  exact i hi

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 1
i : ℕ
hi : autoParam (i + 2 ≤ 1) _auto✝
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 1
i : ℕ
hi : autoParam (i + 2 ≤ 1) _auto✝
⊢ (S.sc ⋯ i ⋯).Exact

Tactic:
exfalso

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 1
i : ℕ
hi : autoParam (i + 2 ≤ 1) _auto✝
⊢ False
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem cocycle_snd_snd (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd _ _ ≫ pullback.snd _ _ =
      pullback.snd _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)

Tactic:
simp only [t'_snd_snd, t'_fst_fst_fst, t'_fst_snd]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem HasDerivAt.le_of_lip' {f : 𝕜 → F} {f' : F} {x₀ : 𝕜} (hf : HasDerivAt f f' x₀)
    {C : ℝ} (hC₀ : 0 ≤ C) (hlip : ∀ᶠ x in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) :
    ‖f'‖ ≤ C

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x₀ : 𝕜
hf : HasDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ‖f'‖ ≤ C

Tactic:
simpa using HasFDerivAt.le_of_lip' hf.hasFDerivAt hC₀ hlip

Result:
no goals
-- Mathlib/RingTheory/Norm/Transitivity.lean
theorem comp_det_mul_pow :
    ((M.map f).comp m m n n R).det * (f (M k k)).det ^ (Fintype.card m - 1) =
      (f (M k k)).det * (((mulAuxMatBlock).map f).comp _ _ n n R).det

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      ((blockDiagonal fun m => f (M k k)).det * (blockDiagonal fun m => f 1).det)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    (f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x => x = k) False).map ⇑f)).det

Tactic:
trans (((M * auxMat M k).map f).comp m m n n R).det

Result:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) ((M * auxMat M k).map ⇑f)).det

R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) ((M * auxMat M k).map ⇑f)).det =
    (f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x => x = k) False).map ⇑f)).det

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (blockDiagonal fun m => f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x => x = k) False).map ⇑f)).det =
    (f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x => x = k) False).map ⇑f)).det

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem one_lt_div' : 1 < a / b ↔ b < a

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ 1 < a / b ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_C (r : R) (hk : 0 < k) : hasseDeriv k (C r) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
r : R
hk : 0 < k
⊢ (hasseDeriv k) (C r) = 0

Tactic:
rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
  zero_mul, monomial_zero_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n

Proof state:
s n m : Nat
⊢ (∃ i, i < n ∧ m = s + i) ↔ s ≤ m ∧ m < s + n

Tactic:
exact ⟨
fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩

Result:
no goals

Proof state:
s n m : Nat
⊢ m ∈ range' s n ↔ s ≤ m ∧ m < s + n

Tactic:
simp [mem_range']

Result:
s n m : Nat
⊢ (∃ i, i < n ∧ m = s + i) ↔ s ≤ m ∧ m < s + n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_or_distrib_left (x y z : Nat) : x &&& (y ||| z) = (x &&& y) ||| (x &&& z)

Proof state:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x &&& (y ||| z)).testBit i = (x &&& y ||| x &&& z).testBit i

Tactic:
simp [Bool.and_or_distrib_left]

Result:
no goals

Proof state:
x y z : Nat
⊢ x &&& (y ||| z) = x &&& y ||| x &&& z

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x &&& (y ||| z)).testBit i = (x &&& y ||| x &&& z).testBit i
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_hom₂ [CommMonoid γ] (s : Multiset ι) (f : α → β → γ)
    (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → α)
    (f₂ : ι → β) : (s.map fun i => f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod :=
  Quotient.inductionOn s fun l => by
    simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, map_coe, prod_coe]

Proof state:
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_6
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
s : Multiset ι
f : α → β → γ
hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → α
f₂ : ι → β
l : List ι
⊢ (map (fun i => f (f₁ i) (f₂ i)) ⟦l⟧).prod = f (map f₁ ⟦l⟧).prod (map f₂ ⟦l⟧).prod

Tactic:
simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, map_coe, prod_coe]

Result:
no goals
-- Mathlib/Data/List/Lattice.lean
theorem inter_eq_nil_iff_disjoint : l₁ ∩ l₂ = [] ↔ Disjoint l₁ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
⊢ (∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ l₁.Disjoint l₂

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
⊢ l₁ ∩ l₂ = [] ↔ l₁.Disjoint l₂

Tactic:
simp only [eq_nil_iff_forall_not_mem, mem_inter_iff, not_and]

Result:
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
⊢ (∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ l₁.Disjoint l₂
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
lemma δ_L₃_f : S.δ ≫ S.L₃.f = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.δ ≫ S.L₃.f = 0

Tactic:
erw [← cancel_epi S.L₀'.g, S.L₀'_exact.g_desc_assoc, assoc, S.v₂₃.comm₁₂, S.φ₁_L₂_f_assoc,
  φ₂, assoc, w₁₃_τ₂, comp_zero, comp_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_swapAt (a : Array α) (i : Nat) (v : α) (hi) :
    (a.swapAt i v hi).2.size = a.size

Proof state:
α : Type u_1
a : Array α
i : Nat
v : α
hi : i < a.size
⊢ (a.swapAt i v hi).snd.size = a.size

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem one_le {I : FractionalIdeal S P} : 1 ≤ I ↔ (1 : P) ∈ I

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
⊢ 1 ≤ I ↔ 1 ∈ I

Tactic:
rw [← coe_le_coe, coe_one, Submodule.one_le, mem_coe]

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem map_mul_left_nhds_one₀ (ha : a ≠ 0) : map (a * ·) (𝓝 1) = 𝓝 (a)

Proof state:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ map (fun x => a * x) (𝓝 1) = 𝓝 a

Tactic:
rw [map_mul_left_nhds₀ ha, mul_one]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_symmDiff [Fintype (s ∆ t : Set _)] :
    (s ∆ t).toFinset = s.toFinset ∆ t.toFinset

Proof state:
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∆ t)
⊢ (s ∆ t).toFinset = s.toFinset ∆ t.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∆ t)
a✝ : α
⊢ a✝ ∈ (s ∆ t).toFinset ↔ a✝ ∈ s.toFinset ∆ t.toFinset

Proof state:
case h
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∆ t)
a✝ : α
⊢ a✝ ∈ (s ∆ t).toFinset ↔ a✝ ∈ s.toFinset ∆ t.toFinset

Tactic:
simp [mem_symmDiff, Finset.mem_symmDiff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean
theorem pullbackObjIso_inv_comp_snd (f : F ⟶ H) (g : G ⟶ H) (d : D) :
    (pullbackObjIso f g d).inv ≫ (pullback.snd f g).app d = pullback.snd (f.app d) (g.app d)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPullbacks C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ (pullbackObjIso f g d).inv ≫ (pullback.snd f g).app d = pullback.snd (f.app d) (g.app d)

Tactic:
simp [pullbackObjIso]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem le_nhds_of_cauchy_adhp {f : Filter α} {x : α} (hf : Cauchy f) (adhs : ClusterPt x f) :
    f ≤ 𝓝 x :=
  le_nhds_of_cauchy_adhp_aux
    (fun s hs => by
      obtain ⟨t, t_mem, ht⟩ : ∃ t ∈ f, t ×ˢ t ⊆ s := (cauchy_iff.1 hf).2 s hs
      use t, t_mem, ht
      exact forall_mem_nonempty_iff_neBot.2 adhs _ (inter_mem_inf (mem_nhds_left x hs) t_mem))

Proof state:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t

Tactic:
obtain ⟨t, t_mem, ht⟩ : ∃ t ∈ f, t ×ˢ t ⊆ s := (cauchy_iff.1 hf).2 s hs

Result:
case intro.intro
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t

Proof state:
case right
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ y, (x, y) ∈ s ∧ y ∈ t

Tactic:
exact forall_mem_nonempty_iff_neBot.2 adhs _ (inter_mem_inf (mem_nhds_left x hs) t_mem)

Result:
no goals

Proof state:
case intro.intro
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t

Tactic:
use t, t_mem, ht

Result:
case right
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ y, (x, y) ∈ s ∧ y ∈ t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_not (x : BitVec w) :
    (~~~x).toFin = x.toFin.rev

Proof state:
w : Nat
x : BitVec w
⊢ ↑(~~~x).toFin = ↑x.toFin.rev

Tactic:
simp only [val_toFin, toNat_not, Fin.val_rev]

Result:
w : Nat
x : BitVec w
⊢ 2 ^ w - 1 - x.toNat = 2 ^ w - (x.toNat + 1)

Proof state:
w : Nat
x : BitVec w
⊢ (~~~x).toFin = x.toFin.rev

Tactic:
apply Fin.val_inj.mp

Result:
w : Nat
x : BitVec w
⊢ ↑(~~~x).toFin = ↑x.toFin.rev

Proof state:
w : Nat
x : BitVec w
⊢ 2 ^ w - 1 - x.toNat = 2 ^ w - (x.toNat + 1)

Tactic:
omega

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_prime_prime_pow {q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime]
    (n : ℕ) (neq : p ≠ q) : padicValNat p (q ^ n) = 0

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n : ℕ
neq : p ≠ q
⊢ padicValNat p (q ^ n) = 0

Tactic:
rw [padicValNat.pow _ <| Nat.Prime.ne_zero hq.elim, padicValNat_primes neq, mul_zero]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracketWithin_eq_zero_of_eq_zero (hV : V x = 0) (hW : W x = 0) :
    lieBracketWithin 𝕜 V W s x = 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
hV : V x = 0
hW : W x = 0
⊢ lieBracketWithin 𝕜 V W s x = 0

Tactic:
simp [lieBracketWithin, hV, hW]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single
    [DecidableEq ι] [∀ i, DecidableEq (G i)] (hV : IsHilbertSum 𝕜 G V) (W₀ : Π₀ i : ι, G i) :
    hV.linearIsometryEquiv.symm (W₀.sum (lp.single 2)) = W₀.sum fun i => V i

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝² : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ hV.linearIsometryEquiv.symm (W₀.sum (lp.single 2)) = W₀.sum fun i => ⇑(V i)

Tactic:
simp only [map_dfinsupp_sum, IsHilbertSum.linearIsometryEquiv_symm_apply_single]

Result:
no goals
-- Mathlib/Analysis/Complex/UnitDisc/Basic.lean
theorem normSq_lt_one (z : 𝔻) : normSq z < 1

Proof state:
z : 𝔻
⊢ normSq ↑z < 1

Tactic:
convert (Real.sqrt_lt' one_pos).1 z.norm_lt_one

Result:
case h.e'_4
z : 𝔻
⊢ 1 = 1 ^ 2

Proof state:
case h.e'_4
z : 𝔻
⊢ 1 = 1 ^ 2

Tactic:
exact (one_pow 2).symm

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_one (x : α) : ∑ i ∈ range 1, x ^ i = 1

Proof state:
α : Type u
inst✝ : Semiring α
x : α
⊢ ∑ i ∈ range 1, x ^ i = 1

Tactic:
simp [geom_sum_succ']

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_sub_const_Ioi : (fun x => x - a) ⁻¹' Ioi b = Ioi (b + a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => x - a) ⁻¹' Ioi b = Ioi (b + a)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem lift_mrange_le {N} [Monoid N] (f : ∀ i, M i →* N) {s : Submonoid N} :
    MonoidHom.mrange (lift f) ≤ s ↔ ∀ i, MonoidHom.mrange (f i) ≤ s

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
s : Submonoid N
⊢ MonoidHom.mrange (lift f) ≤ s ↔ ∀ (i : ι), MonoidHom.mrange (f i) ≤ s

Tactic:
simp [mrange_eq_iSup]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem mul_rpow_of_ne_top {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) (z : ℝ) :
    (x * y) ^ z = x ^ z * y ^ z

Proof state:
x y : ℝ≥0∞
hx : x ≠ ⊤
hy : y ≠ ⊤
z : ℝ
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
simp [*, mul_rpow_eq_ite]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem inv₀ {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint x⁻¹

Proof state:
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint x⁻¹

Tactic:
simp only [isSelfAdjoint_iff, star_inv₀, hx.star_eq]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem vadd_vsub_assoc (g : G) (p₁ p₂ : P) : (g +ᵥ p₁) -ᵥ p₂ = g + (p₁ -ᵥ p₂)

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g : G
p₁ p₂ : P
⊢ ((g +ᵥ p₁) -ᵥ p₂) +ᵥ p₂ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂

Tactic:
rw [vsub_vadd, add_vadd, vsub_vadd]

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g : G
p₁ p₂ : P
⊢ (g +ᵥ p₁) -ᵥ p₂ = g + (p₁ -ᵥ p₂)

Tactic:
apply vadd_right_cancel p₂

Result:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g : G
p₁ p₂ : P
⊢ ((g +ᵥ p₁) -ᵥ p₂) +ᵥ p₂ = (g + (p₁ -ᵥ p₂)) +ᵥ p₂
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    get! m a = (get? m a).get!

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
a : α
⊢ get! m a = (get? m a).get!

Tactic:
simp_to_raw using Raw₀.Const.get!_eq_get!_get?

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_sub_const (v₁ v₂ v₃ : V) (v : V) : ∠ (v₁ - v) (v₂ - v) (v₃ - v) = ∠ v₁ v₂ v₃

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
v₁ v₂ v₃ v : V
⊢ ∠ (v₁ - v) (v₂ - v) (v₃ - v) = ∠ v₁ v₂ v₃

Tactic:
simpa only [vsub_eq_sub] using angle_vsub_const v₁ v₂ v₃ v

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobjectMap_id : kernelSubobjectMap (𝟙 (Arrow.mk f)) = 𝟙 _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ kernelSubobjectMap (𝟙 (Arrow.mk f)) = 𝟙 (underlying.obj (kernelSubobject f))

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bfamilyOfFamily'_typein {ι} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (i) :
    bfamilyOfFamily' r f (typein r i) (typein_lt_type r i) = f i

Proof state:
α : Type u_1
ι : Type u_4
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
i : ι
⊢ bfamilyOfFamily' r f ((typein r).toRelEmbedding i) ⋯ = f i

Tactic:
simp only [bfamilyOfFamily', enum_typein]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem pathComponent_subset_component (x : X) : pathComponent x ⊆ connectedComponent x :=
  fun y h =>
  (isConnected_range h.somePath.continuous).subset_connectedComponent ⟨0, by simp⟩ ⟨1, by simp⟩

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : y ∈ pathComponent x
⊢ (Joined.somePath h) 1 = y

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : y ∈ pathComponent x
⊢ (Joined.somePath h) 0 = x

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iio_subset_Iio (h : a ≤ b) : Iio a ⊆ Iio b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iio a ⊆ Iio b

Tactic:
simpa [← coe_subset] using Set.Iio_subset_Iio h

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
private lemma aux_sub (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
    a * (f x - m / (2 : ℝ) * ‖x‖ ^ 2) + b * (f y - m / (2 : ℝ) * ‖y‖ ^ 2) +
      m / (2 : ℝ) * ‖a • x + b • y‖ ^ 2
      = a * f x + b * f y - m / (2 : ℝ) * a * b * ‖x - y‖ ^ 2

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) +
      m / 2 * (a ^ 2 * ‖x‖ ^ 2 + 2 * (a * (b * inner x y)) + b ^ 2 * ‖y‖ ^ 2) =
    a * f x + b * f y - m / 2 * a * b * (‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2)

Tactic:
obtain rfl := eq_sub_of_add_eq hab

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
b m : ℝ
x y : E
f : E → ℝ
hb : 0 ≤ b
ha : 0 ≤ 1 - b
hab : 1 - b + b = 1
⊢ (1 - b) * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) +
      m / 2 * ((1 - b) ^ 2 * ‖x‖ ^ 2 + 2 * ((1 - b) * (b * inner x y)) + b ^ 2 * ‖y‖ ^ 2) =
    (1 - b) * f x + b * f y - m / 2 * (1 - b) * b * (‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) + m / 2 * ‖a • x + b • y‖ ^ 2 =
    a * f x + b * f y - m / 2 * a * b * ‖x - y‖ ^ 2

Tactic:
rw [norm_add_sq_real, norm_sub_sq_real, norm_smul, norm_smul, real_inner_smul_left,
  inner_smul_right, norm_of_nonneg ha, norm_of_nonneg hb, mul_pow, mul_pow]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) +
      m / 2 * (a ^ 2 * ‖x‖ ^ 2 + 2 * (a * (b * inner x y)) + b ^ 2 * ‖y‖ ^ 2) =
    a * f x + b * f y - m / 2 * a * b * (‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
b m : ℝ
x y : E
f : E → ℝ
hb : 0 ≤ b
ha : 0 ≤ 1 - b
hab : 1 - b + b = 1
⊢ (1 - b) * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) +
      m / 2 * ((1 - b) ^ 2 * ‖x‖ ^ 2 + 2 * ((1 - b) * (b * inner x y)) + b ^ 2 * ‖y‖ ^ 2) =
    (1 - b) * f x + b * f y - m / 2 * (1 - b) * b * (‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2)

Tactic:
ring_nf

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem insert_diff_singleton_comm (hab : a ≠ b) (s : Set α) :
    insert a (s \ {b}) = insert a s \ {b}

Proof state:
α : Type u
a b : α
hab : a ≠ b
s : Set α
⊢ insert a (s \ {b}) = insert a s \ {b}

Tactic:
simp_rw [← union_singleton, union_diff_distrib,
  diff_singleton_eq_self (mem_singleton_iff.not.2 hab.symm)]

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem zipRight_nil_left : zipRight ([] : List α) bs = bs.map fun b => (none, b)

Proof state:
α : Type u
β : Type v
bs : List β
⊢ [].zipRight bs = map (fun b => (none, b)) bs

Tactic:
cases bs <;> rfl

Result:
no goals