harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean
theorem FiniteField.isSquare_neg_two_iff :
    IsSquare (-2 : F) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Proof state:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 3 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
omega

Result:
no goals

Proof state:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
simp only [FiniteField.isSquare_of_char_two hF, true_iff]

Result:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Proof state:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (Ring.two_ne_zero hF)),
  quadraticChar_neg_two hF, χ₈'_nat_eq_if_mod_eight]

Result:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 3 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
by_cases hF : ringChar F = 2

Result:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Proof state:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
have h := FiniteField.odd_card_of_char_ne_two hF

Result:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Proof state:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
have h := FiniteField.even_card_of_char_two hF

Result:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Proof state:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma homMk'_mk_comp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
    homMk' (mk f) (g ≫ g') = homMk' (mk f) g ≫ homMk' (mk (f ≫ T.map g)) g' ≫ eqToHom (by simp) :=
  homMk'_comp _ _ _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((mk (f ≫ T.map g)).hom ≫ T.map g') = mk ((mk f).hom ≫ T.map (g ≫ g'))

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_eq_top_of_infinite [Infinite α] : card α = ⊤

Proof state:
α : Type u_1
inst✝ : Infinite α
⊢ card α = ⊤

Tactic:
simp only [card, toENat_eq_top, aleph0_le_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_self : ∀ n, subNatNat n n = 0
  | 0      => rfl
  | succ m => by rw [subNatNat_of_sub_eq_zero (Nat.sub_self ..), Nat.sub_self, ofNat_zero]

Proof state:
m : Nat
⊢ subNatNat m.succ m.succ = 0

Tactic:
rw [subNatNat_of_sub_eq_zero (Nat.sub_self ..), Nat.sub_self, ofNat_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem lt_iff_le_and_exists (s₁ s₂ : AffineSubspace k P) :
    s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁

Tactic:
rw [lt_iff_le_not_le, not_le_iff_exists]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_mul_apply_of_coprime {p a b : ℕ} (hab : Coprime a b) :
    (a * b).factorization p = a.factorization p + b.factorization p

Proof state:
p a b : ℕ
hab : a.Coprime b
⊢ (a * b).factorization p = a.factorization p + b.factorization p

Tactic:
simp only [← primeFactorsList_count_eq,
  perm_iff_count.mp (perm_primeFactorsList_mul_of_coprime hab), count_append]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_add_natCast' (hx : 0 ≤ x) (h : y + n ≠ 0) : x ^ (y + n) = x ^ y * x ^ n

Proof state:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y + ↑n ≠ 0
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
rw [rpow_add' hx h, rpow_natCast]

Result:
no goals
-- Mathlib/Data/Set/Functor.lean
theorem image2_def {α β γ : Type u} (f : α → β → γ) (s : Set α) (t : Set β) :
    image2 f s t = f <$> s <*> t

Proof state:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = f <$> s <*> t

Tactic:
ext

Result:
case h
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ f <$> s <*> t

Proof state:
case h
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ f <$> s <*> t

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_or_eq_of_mem_set
    {as : Array α} {i : Nat} {a b : α} {w : i < as.size} (h : a ∈ as.set i b) : a ∈ as ∨ a = b

Proof state:
α : Type u_1
as : Array α
i : Nat
a b : α
w : i < as.size
h : a ∈ as.set i b w
⊢ a ∈ as ∨ a = b

Tactic:
cases as

Result:
case mk
α : Type u_1
i : Nat
a b : α
toList✝ : List α
w : i < { toList := toList✝ }.size
h : a ∈ { toList := toList✝ }.set i b w
⊢ a ∈ { toList := toList✝ } ∨ a = b

Proof state:
case mk
α : Type u_1
i : Nat
a b : α
toList✝ : List α
w : i < { toList := toList✝ }.size
h : a ∈ { toList := toList✝ }.set i b w
⊢ a ∈ { toList := toList✝ } ∨ a = b

Tactic:
simpa using List.mem_or_eq_of_mem_set (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
i : Nat
a b : α
toList✝ : List α
w : i < { toList := toList✝ }.size
h : a ∈ { toList := toList✝ }.set i b w
⊢ a ∈ toList✝.set ?m.129320 b

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem tendsto_lift₂_nhdsWithin {f : X → Y → α}
    {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} {x : X} {y : Y}
    {s : Set (SeparationQuotient X × SeparationQuotient Y)} {l : Filter α} :
    Tendsto (uncurry <| lift₂ f hf) (𝓝[s] (mk x, mk y)) l ↔
      Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l

Proof state:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (Filter.map (Prod.map mk mk) (𝓝 (x, y) ⊓ 𝓟 (Prod.map mk mk ⁻¹' s))) l ↔
    Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝[s] (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l

Tactic:
rw [nhdsWithin, ← map_prod_map_mk_nhds, ← Filter.push_pull, comap_principal]

Result:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (Filter.map (Prod.map mk mk) (𝓝 (x, y) ⊓ 𝓟 (Prod.map mk mk ⁻¹' s))) l ↔
    Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
-- Mathlib/Analysis/Convex/Basic.lean
theorem convex_iff_pairwise_pos : Convex 𝕜 s ↔
    s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ Convex 𝕜 s ↔ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
refine convex_iff_forall_pos.trans ⟨fun h x hx y hy _ => h hx hy, ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ (s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) →
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Tactic:
obtain rfl | hxy := eq_or_ne x y

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hy : x ∈ s
⊢ a • x + b • x ∈ s

case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x ≠ y
⊢ a • x + b • y ∈ s

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x ≠ y
⊢ a • x + b • y ∈ s

Tactic:
exact h hx hy hxy ha hb hab

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hy : x ∈ s
⊢ a • x + b • x ∈ s

Tactic:
rwa [Convex.combo_self hab]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ (s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) →
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
intro h x hx y hy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ s
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@[simp]
lemma map_id : map S f f (.id ) = .id

Proof state:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
⊢ ((map S f f) LinearMap.id) x = LinearMap.id x

Tactic:
obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x

Result:
case h.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M
s : ↥S
⊢ ((map S f f) LinearMap.id) (Function.uncurry (mk' f) (x, s)) = LinearMap.id (Function.uncurry (mk' f) (x, s))

Proof state:
case h.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M
s : ↥S
⊢ ((map S f f) LinearMap.id) (Function.uncurry (mk' f) (x, s)) = LinearMap.id (Function.uncurry (mk' f) (x, s))

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
⊢ (map S f f) LinearMap.id = LinearMap.id

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
⊢ ((map S f f) LinearMap.id) x = LinearMap.id x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_dropLast {xs : List α} (h) :
   xs.dropLast.getLast h =
     xs[xs.length - 2]'(match xs, h with | (_ :: _ :: _), _ => Nat.lt_trans (Nat.lt_add_one _) (Nat.lt_add_one _))

Proof state:
case e_i
α : Type u_1
xs : List α
h : xs.dropLast ≠ []
⊢ xs.dropLast.length - 1 = xs.length - 2

Tactic:
simp

Result:
case e_i
α : Type u_1
xs : List α
h : xs.dropLast ≠ []
⊢ xs.length - 1 - 1 = xs.length - 2

Proof state:
α : Type u_1
xs : List α
h : xs.dropLast ≠ []
⊢ xs[xs.dropLast.length - 1] = xs[xs.length - 2]

Tactic:
congr 1

Result:
case e_i
α : Type u_1
xs : List α
h : xs.dropLast ≠ []
⊢ xs.dropLast.length - 1 = xs.length - 2

Proof state:
case e_i
α : Type u_1
xs : List α
h : xs.dropLast ≠ []
⊢ xs.length - 1 - 1 = xs.length - 2

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
xs : List α
h : xs.dropLast ≠ []
⊢ xs.dropLast.getLast h = xs[xs.length - 2]

Tactic:
rw [getLast_eq_getElem, getElem_dropLast]

Result:
α : Type u_1
xs : List α
h : xs.dropLast ≠ []
⊢ xs[xs.dropLast.length - 1] = xs[xs.length - 2]
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_bot {f : α → β} {l : Filter β} : Tendsto f ⊥ l

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
⊢ Tendsto f ⊥ l

Tactic:
simp [Tendsto]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_int_le_one (z : ℤ) : ‖(z : ℚ_[p])‖ ≤ 1 :=
  suffices ‖((z : ℚ) : ℚ_[p])‖ ≤ 1 by simpa
  norm_rat_le_one <| by simp [hp.1.ne_one]

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ¬p ∣ (↑z).den

Tactic:
simp [hp.1.ne_one]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
this : ‖↑↑z‖ ≤ 1
⊢ ‖↑z‖ ≤ 1

Tactic:
simpa

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
@[reassoc (attr := simp)]
lemma hom_inv_id_left (e : f ≅ g) : e.hom.left ≫ e.inv.left = 𝟙 _

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ e.hom.left ≫ e.inv.left = 𝟙 f.left

Tactic:
rw [← comp_left, e.hom_inv_id, id_left]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
theorem IsIntegralClosure.finite [IsIntegrallyClosed A] [IsNoetherianRing A] :
    Module.Finite A C

Proof state:
A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
⊢ Module.Finite A C

Tactic:
haveI := IsIntegralClosure.isNoetherian A K L C

Result:
A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this : IsNoetherian A C
⊢ Module.Finite A C

Proof state:
A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this : IsNoetherian A C
⊢ Module.Finite A C

Tactic:
exact Module.IsNoetherian.finite A C

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
@[simp] lemma subsemiringClosure_toNonUnitalSubsemiring (M : Submonoid R) :
    M.subsemiringClosure.toNonUnitalSubsemiring = .closure M

Proof state:
case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ AddSubmonoid.closure ↑M
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
induction hx using AddSubmonoid.closure_induction <;> aesop

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
simp [Submonoid.subsemiringClosure_mem] at hx

Result:
case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ AddSubmonoid.closure ↑M
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ M.subsemiringClosure.toNonUnitalSubsemiring = NonUnitalSubsemiring.closure ↑M

Tactic:
refine Eq.symm (NonUnitalSubsemiring.closure_eq_of_le ?_ fun _ hx ↦ ?_)

Result:
case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ ↑M ⊆ ↑M.subsemiringClosure.toNonUnitalSubsemiring

case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Proof state:
case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ ↑M ⊆ ↑M.subsemiringClosure.toNonUnitalSubsemiring

Tactic:
simp [Submonoid.subsemiringClosure_coe]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Defs.lean
theorem transcendental_iff {x : A} :
    Transcendental R x ↔ ∀ p : R[X], aeval x p = 0 → p = 0

Proof state:
case a.h.a
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
a✝ : R[X]
⊢ ¬(a✝ ≠ 0 ∧ (aeval x) a✝ = 0) ↔ (aeval x) a✝ = 0 → a✝ = 0

Tactic:
tauto

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ Transcendental R x ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0

Tactic:
rw [Transcendental, IsAlgebraic, not_exists]

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ (∀ (x_1 : R[X]), ¬(x_1 ≠ 0 ∧ (aeval x) x_1 = 0)) ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ (∀ (x_1 : R[X]), ¬(x_1 ≠ 0 ∧ (aeval x) x_1 = 0)) ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0

Tactic:
congr! 1

Result:
case a.h.a
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
a✝ : R[X]
⊢ ¬(a✝ ≠ 0 ∧ (aeval x) a✝ = 0) ↔ (aeval x) a✝ = 0 → a✝ = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem mul_eval (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₁.coeffs.isZero ∨ l₂.coeffs.isZero) :
    (mul l₁ l₂).eval v = l₁.eval v * l₂.eval v

Proof state:
l₁ l₂ : LinearCombo
v : Coeffs
w : l₁.coeffs.isZero ∨ l₂.coeffs.isZero
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

Tactic:
rcases w with w | w

Result:
case inl
l₁ l₂ : LinearCombo
v : Coeffs
w : l₁.coeffs.isZero
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

case inr
l₁ l₂ : LinearCombo
v : Coeffs
w : l₂.coeffs.isZero
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

Proof state:
case inl
l₁ l₂ : LinearCombo
v : Coeffs
w : l₁.coeffs.isZero
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

Tactic:
rw [mul_eval_of_const_left _ _ _ w]

Result:
no goals

Proof state:
case inr
l₁ l₂ : LinearCombo
v : Coeffs
w : l₂.coeffs.isZero
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

Tactic:
rw [mul_eval_of_const_right _ _ _ w]

Result:
no goals
-- Mathlib/Order/DirectedInverseSystem.lean
theorem piEquivSucc_self {x} :
    piEquivSucc equiv e hi ⟨_, le_rfl⟩ x ⟨i, lt_succ_of_not_isMax hi⟩ = (e x).2

Proof state:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : LinearOrder ι
inst✝ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
x : F ↑⟨i⁺, ⋯⟩
⊢ (piEquivSucc equiv e hi ⟨i⁺, ⋯⟩) x ⟨i, ⋯⟩ = (e x).2

Tactic:
simp [piEquivSucc]

Result:
no goals
-- Mathlib/ModelTheory/Syntax.lean
theorem mapTermRel_id_id_id {n} (φ : L.BoundedFormula α n) :
    (φ.mapTermRel (fun _ => id) (fun _ => id) fun _ => id) = φ

Proof state:
case falsum
L : Language
α : Type u'
n n✝ : ℕ
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) falsum = falsum

Tactic:
rfl

Result:
no goals

Proof state:
case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : mapTermRel (fun x => id) (fun x => id) (fun x => id) f₁✝ = f₁✝
ih2 : mapTermRel (fun x => id) (fun x => id) (fun x => id) f₂✝ = f₂✝
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) (f₁✝.imp f₂✝) = f₁✝.imp f₂✝

Tactic:
simp [mapTermRel, ih1, ih2]

Result:
no goals

Proof state:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) φ = φ

Tactic:
induction φ with
| falsum => rfl
| equal => simp [mapTermRel]
| rel => simp [mapTermRel]
| imp _ _ ih1 ih2 => simp [mapTermRel, ih1, ih2]
| all _ ih3 => simp [mapTermRel, ih3]

Result:
no goals

Proof state:
case equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) (equal t₁✝ t₂✝) = equal t₁✝ t₂✝

Tactic:
simp [mapTermRel]

Result:
no goals

Proof state:
case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) (rel R✝ ts✝) = rel R✝ ts✝

Tactic:
simp [mapTermRel]

Result:
no goals

Proof state:
case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : mapTermRel (fun x => id) (fun x => id) (fun x => id) f✝ = f✝
⊢ mapTermRel (fun x => id) (fun x => id) (fun x => id) f✝.all = f✝.all

Tactic:
simp [mapTermRel, ih3]

Result:
no goals