harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/PrimitiveElement.lean
theorem primitive_element_iff_algHom_eq_of_eval' (α : E) :
    F⟮α⟯ = ⊤ ↔ Function.Injective fun φ : E →ₐ[F] A ↦ φ α

Proof state:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
⊢ F⟮α⟯ = ⊤ ↔ Function.Injective fun φ => φ α

Tactic:
simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
  (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
  ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
  ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
  Finset.coe_univ, ← injective_iff_injOn_univ]

Result:
no goals

Proof state:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
⊢ F⟮α⟯ = ⊤ ↔ Function.Injective fun φ => φ α

Tactic:
classical
simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
  (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
  ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
  ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
  Finset.coe_univ, ← injective_iff_injOn_univ]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem continuous_pow (hf : Continuous f) (n : ℕ) : Continuous (f ^ n : CircleDeg1Lift)

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
n : ℕ
⊢ Continuous ⇑(f ^ n)

Tactic:
rw [coe_pow]

Result:
f : CircleDeg1Lift
hf : Continuous ⇑f
n : ℕ
⊢ Continuous (⇑f)^[n]

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
n : ℕ
⊢ Continuous (⇑f)^[n]

Tactic:
exact hf.iterate n

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
/-- In a flatten of sublists, taking the slice between the indices `A` and `B - 1` gives back the
original sublist of index `i` if `A` is the sum of the lengths of sublists of index `< i`, and
`B` is the sum of the lengths of sublists of index `≤ i`. -/
lemma drop_take_succ_flatten_eq_getElem (L : List (List α)) (i : Nat) (h : i < L.length) :
    (L.flatten.take ((L.map length).take (i + 1)).sum).drop ((L.map length).take i).sum = L[i]

Proof state:
α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
this : take i (map length L) = take i (map length (take (i + 1) L))
⊢ drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) = L[i]

Tactic:
simp only [this, length_map, take_sum_flatten, drop_sum_flatten,
  drop_take_succ_eq_cons_getElem, h, flatten, append_nil]

Result:
no goals

Proof state:
α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
⊢ drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) = L[i]

Tactic:
have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
  simp [map_take, take_take, Nat.min_eq_left]

Result:
α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
this : take i (map length L) = take i (map length (take (i + 1) L))
⊢ drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) = L[i]

Proof state:
α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
⊢ take i (map length L) = take i (map length (take (i + 1) L))

Tactic:
simp [map_take, take_take, Nat.min_eq_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getD_eq_get? (a : Array α) (i d) : a.getD i d = (a[i]?).getD d

Proof state:
α : Type u_1
a : Array α
i : Nat
d : α
⊢ a.getD i d = a[i]?.getD d

Tactic:
simp only [getD, get_eq_getElem, get?_eq_getElem?]

Result:
α : Type u_1
a : Array α
i : Nat
d : α
⊢ (if h : i < a.size then a[i] else d) = a[i]?.getD d

Proof state:
α : Type u_1
a : Array α
i : Nat
d : α
⊢ (if h : i < a.size then a[i] else d) = a[i]?.getD d

Tactic:
split <;> simp [getD_getElem?, *]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem permutationsAux2_snd_eq (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β) :
    (permutationsAux2 t ts r ys f).2 =
      ((permutationsAux2 t [] [] ys id).2.map fun x => f (x ++ ts)) ++ r

Proof state:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r ys f).2 = map (fun x => f (x ++ ts)) (permutationsAux2 t [] [] ys id).2 ++ r

Tactic:
rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]

Result:
no goals
-- Mathlib/Logic/Lemmas.lean
lemma Prop.forall {f : Prop → Prop} : (∀ p, f p) ↔ f True ∧ f False :=
  ⟨fun h ↦ ⟨h _, h _⟩, by rintro ⟨h₁, h₀⟩ p; by_cases hp : p <;> simp only [hp] <;> assumption⟩

Proof state:
f : Prop → Prop
⊢ f True ∧ f False → ∀ (p : Prop), f p

Tactic:
rintro ⟨h₁, h₀⟩ p

Result:
case intro
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
⊢ f p

Proof state:
case intro
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
⊢ f p

Tactic:
by_cases hp : p <;> simp only [hp] <;> assumption

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem essSup_le_of_ae_le {f : α → β} (c : β) (hf : f ≤ᵐ[μ] fun _ => c) : essSup f μ ≤ c :=
  limsup_le_of_le (by isBoundedDefault) hf

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᶠ[ae μ] fun x => c
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f

Tactic:
isBoundedDefault

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma norm_log_natCast_le_rpow_div (n : ℕ) {ε : ℝ} (hε : 0 < ε) : ‖log n‖ ≤ n ^ ε / ε

Proof state:
case inl
ε : ℝ
hε : 0 < ε
⊢ ‖log ↑0‖ ≤ ↑0 ^ ε / ε

Tactic:
rw [Nat.cast_zero, Nat.cast_zero, log_zero, norm_zero, Real.zero_rpow hε.ne', zero_div]

Result:
no goals

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
⊢ ‖log ↑n‖ ≤ ↑n ^ ε / ε

Tactic:
rcases n.eq_zero_or_pos with rfl | h

Result:
case inl
ε : ℝ
hε : 0 < ε
⊢ ‖log ↑0‖ ≤ ↑0 ^ ε / ε

case inr
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ ‖log ↑n‖ ≤ ↑n ^ ε / ε

Proof state:
case inr
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ ‖log ↑n‖ ≤ ↑n ^ ε / ε

Tactic:
rw [← natCast_log, norm_real, norm_of_nonneg <| Real.log_nonneg <| by
  exact_mod_cast Nat.one_le_of_lt h.lt]

Result:
case inr
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ Real.log ↑n ≤ ↑n ^ ε / ε

Proof state:
case inr
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ Real.log ↑n ≤ ↑n ^ ε / ε

Tactic:
exact Real.log_natCast_le_rpow_div n hε

Result:
no goals

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ 1 ≤ ↑n

Tactic:
exact_mod_cast Nat.one_le_of_lt h.lt

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} (i : δ):
    (zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l₁ : Array α
l₂ : Array β
g : γ → δ → δ
f : α → β → γ
i : δ
⊢ foldr g i (zipWith f l₁ l₂) = foldr (fun p r => g (f p.fst p.snd) r) i (l₁.zip l₂)

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l₂ : Array β
g : γ → δ → δ
f : α → β → γ
i : δ
toList✝ : List α
⊢ foldr g i (zipWith f { toList := toList✝ } l₂) =
    foldr (fun p r => g (f p.fst p.snd) r) i ({ toList := toList✝ }.zip l₂)

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l₂ : Array β
g : γ → δ → δ
f : α → β → γ
i : δ
toList✝ : List α
⊢ foldr g i (zipWith f { toList := toList✝ } l₂) =
    foldr (fun p r => g (f p.fst p.snd) r) i ({ toList := toList✝ }.zip l₂)

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : γ → δ → δ
f : α → β → γ
i : δ
toList✝¹ : List α
toList✝ : List β
⊢ foldr g i (zipWith f { toList := toList✝¹ } { toList := toList✝ }) =
    foldr (fun p r => g (f p.fst p.snd) r) i ({ toList := toList✝¹ }.zip { toList := toList✝ })

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
g : γ → δ → δ
f : α → β → γ
i : δ
toList✝¹ : List α
toList✝ : List β
⊢ foldr g i (zipWith f { toList := toList✝¹ } { toList := toList✝ }) =
    foldr (fun p r => g (f p.fst p.snd) r) i ({ toList := toList✝¹ }.zip { toList := toList✝ })

Tactic:
simp [List.zipWith_foldr_eq_zip_foldr]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValRat_le_padicValRat_iff {n₁ n₂ d₁ d₂ : ℤ} (hn₁ : n₁ ≠ 0) (hn₂ : n₂ ≠ 0)
    (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) :
    padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔
      ∀ n : ℕ, (p : ℤ) ^ n ∣ n₁ * d₂ → (p : ℤ) ^ n ∣ n₂ * d₁

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

Tactic:
have hf1 : FiniteMultiplicity (p : ℤ) (n₁ * d₂) := finite_int_prime_iff.2 (mul_ne_zero hn₁ hd₂)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

Tactic:
have hf2 : FiniteMultiplicity (p : ℤ) (n₂ * d₁) := finite_int_prime_iff.2 (mul_ne_zero hn₂ hd₁)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p) (n₂ * d₁)
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

Tactic:
conv =>
  lhs
  rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
    padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ←
    add_sub_assoc, _root_.le_sub_iff_add_le]
  norm_cast
  rw [← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm,
      ← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf2,
      hf1.multiplicity_le_multiplicity_iff hf2]

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem log_inv (b : ℕ) (r : R) : log b r⁻¹ = -clog b r

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ log b r⁻¹ = -clog b r

Tactic:
rw [← inv_inv r, clog_inv, neg_neg, inv_inv]

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_principal {f : α → β} {l : Filter α} {s : Set β} :
    Tendsto f l (𝓟 s) ↔ ∀ᶠ a in l, f a ∈ s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
s : Set β
⊢ Tendsto f l (𝓟 s) ↔ ∀ᶠ (a : α) in l, f a ∈ s

Tactic:
simp only [Tendsto, le_principal_iff, mem_map', Filter.Eventually]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Int.lean
lemma two_le_iff_pos_of_even {m : ℤ} (even : Even m) : 2 ≤ m ↔ 0 < m :=
  le_iff_pos_of_dvd (by decide) even.two_dvd

Proof state:
m : ℤ
even : Even m
⊢ 0 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/Probability/Moments/ComplexMGF.lean
theorem hasDerivAt_complexMGF (hz : z.re ∈ interior (integrableExpSet X μ)) :
    HasDerivAt (complexMGF X μ) μ[fun ω ↦ X ω * cexp (z * X ω)] z

Proof state:
case h.e'_8.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
x✝ : ℂ
⊢ complexMGF X μ x✝ = ∫ (x : Ω), (fun ω => ↑(X ω) ^ 0 * cexp (x✝ * ↑(X ω))) x ∂μ

Tactic:
simp [complexMGF]

Result:
no goals

Proof state:
case h.e'_9.h.e'_7.h.h.e.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
x✝¹ x✝ : Ω
⊢ ↑(X x✝) = ↑(X x✝) ^ (0 + 1)

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun ω => ↑(X ω) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
convert hasDerivAt_integral_pow_mul_exp hz 0

Result:
case h.e'_8.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
x✝ : ℂ
⊢ complexMGF X μ x✝ = ∫ (x : Ω), (fun ω => ↑(X ω) ^ 0 * cexp (x✝ * ↑(X ω))) x ∂μ

case h.e'_9.h.e'_7.h.h.e.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
x✝¹ x✝ : Ω
⊢ ↑(X x✝) = ↑(X x✝) ^ (0 + 1)
-- Mathlib/Computability/Primrec.lean
theorem unpaired {f : ℕ → ℕ → α} : Primrec (Nat.unpaired f) ↔ Primrec₂ f :=
  ⟨fun h => by simpa using h.comp natPair, fun h => h.comp Primrec.unpair⟩

Proof state:
α : Type u_1
inst✝ : Primcodable α
f : ℕ → ℕ → α
h : Primrec (Nat.unpaired f)
⊢ Primrec₂ f

Tactic:
simpa using h.comp natPair

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem dropn_tail (s : WSeq α) (n) : drop (tail s) n = drop s (n + 1)

Proof state:
α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)

Tactic:
symm

Result:
α : Type u
s : WSeq α
n : ℕ
⊢ s.drop (1 + n) = s.tail.drop n

Proof state:
α : Type u
s : WSeq α
n : ℕ
⊢ s.drop (1 + n) = s.tail.drop n

Tactic:
apply dropn_add

Result:
no goals

Proof state:
α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (n + 1)

Tactic:
rw [Nat.add_comm]

Result:
α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)
-- Mathlib/Analysis/Normed/MulAction.lean
theorem dist_smul₀ (s : α) (x y : β) : dist (s • x) (s • y) = ‖s‖ * dist x y

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) = ‖s‖ * dist x y

Tactic:
simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem cospanExt_hom_app_left :
    (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.left = iX.hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.left = iX.hom

Tactic:
dsimp [cospanExt]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem parallelPair_functor_obj {F : WalkingParallelPair ⥤ C} (j : WalkingParallelPair) :
    (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
cases j <;> rfl

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Degree.lean
theorem intDegree_polynomial {p : K[X]} :
    intDegree (algebraMap K[X] (RatFunc K) p) = natDegree p

Proof state:
K : Type u
inst✝ : Field K
p : K[X]
⊢ ((algebraMap K[X] (RatFunc K)) p).intDegree = ↑p.natDegree

Tactic:
rw [intDegree, RatFunc.num_algebraMap, RatFunc.denom_algebraMap, Polynomial.natDegree_one,
  Int.ofNat_zero, sub_zero]

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isNat_natCast {R} [AddMonoidWithOne R] (n m : ℕ) :
    IsNat n m → IsNat (n : R) m

Proof state:
case mk.refl
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ IsNat (↑↑m) m

Tactic:
exact ⟨rfl⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
n m : ℕ
⊢ IsNat n m → IsNat (↑n) m

Tactic:
rintro ⟨⟨⟩⟩

Result:
case mk.refl
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ IsNat (↑↑m) m
-- Mathlib/CategoryTheory/GradedObject/Associator.lean
@[reassoc (attr := simp)]
lemma ι_mapBifunctorAssociator_inv (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
    ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j =
    ((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝⁹ : Category.{u_13, u_1} C₁
inst✝⁸ : Category.{u_15, u_2} C₂
inst✝⁷ : Category.{u_14, u_5} C₃
inst✝⁶ : Category.{u_11, u_6} C₄
inst✝⁵ : Category.{u_17, u_3} C₁₂
inst✝⁴ : Category.{u_12, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j =
    ((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h

Tactic:
rw [← cancel_mono ((mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j),
  assoc, assoc, Iso.inv_hom_id_eval, comp_id, ι_mapBifunctorAssociator_hom,
  ← NatTrans.comp_app_assoc, ← NatTrans.comp_app, Iso.inv_hom_id_app,
  NatTrans.id_app, NatTrans.id_app, id_comp]

Result:
no goals
-- Mathlib/FieldTheory/KummerPolynomial.lean
lemma root_X_pow_sub_C_eq_zero_iff {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
    (AdjoinRoot.root (X ^ n - C a)) = 0 ↔ a = 0

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
hn : 0 < n
⊢ a = 0 → root (X ^ n - C a) = 0

Tactic:
rintro rfl

Result:
K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
⊢ root (X ^ n - C 0) = 0

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
⊢ root (X ^ n - C a) = 0 ↔ a = 0

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)

Result:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
hn : 0 < n
⊢ root (X ^ n - C a) = 0 ↔ a = 0

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
⊢ root (X ^ n - C 0) = 0

Tactic:
have := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) rfl

Result:
K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ root (X ^ n - C 0) = 0

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
hn : 0 < n
⊢ root (X ^ n - C a) = 0 ↔ a = 0

Tactic:
refine ⟨not_imp_not.mp (root_X_pow_sub_C_ne_zero' hn), ?_⟩

Result:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
hn : 0 < n
⊢ a = 0 → root (X ^ n - C a) = 0

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ root (X ^ n - C 0) = 0

Tactic:
rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]

Result:
no goals
-- Mathlib/Analysis/Convex/Mul.lean
lemma ConvexOn.smul_concaveOn (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g)
    (hf₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x⦄, x ∈ s → g x ≤ 0) (hfg : AntivaryOn f g s) :
    ConcaveOn 𝕜 s (f • g)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : LinearOrderedCommRing 𝕜
inst✝⁸ : LinearOrderedCommRing E
inst✝⁷ : LinearOrderedAddCommGroup F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : OrderedSMul 𝕜 F
inst✝ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConvexOn 𝕜 s (f • -g)

Tactic:
exact hf.smul' hg.neg hf₀ (fun x hx ↦ neg_nonneg.2 <| hg₀ hx) hfg.neg_right

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : LinearOrderedCommRing 𝕜
inst✝⁸ : LinearOrderedCommRing E
inst✝⁷ : LinearOrderedAddCommGroup F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : OrderedSMul 𝕜 F
inst✝ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (f • g)

Tactic:
rw [← neg_convexOn_iff, ← smul_neg]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : LinearOrderedCommRing 𝕜
inst✝⁸ : LinearOrderedCommRing E
inst✝⁷ : LinearOrderedAddCommGroup F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : OrderedSMul 𝕜 F
inst✝ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConvexOn 𝕜 s (f • -g)
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_lineMap_left (p₁ p₂ : P) (c : 𝕜) : dist (lineMap p₁ p₂ c) p₁ = ‖c‖ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist ((lineMap p₁ p₂) c) p₁ = ‖c‖ * dist p₁ p₂

Tactic:
simpa only [lineMap_apply_zero, dist_zero_right] using dist_lineMap_lineMap p₁ p₂ c 0

Result:
no goals
-- Mathlib/Algebra/Exact.lean
@[simp]
lemma exact_zero_iff_injective {M N : Type*} (P : Type*)
    [AddCommGroup M] [AddCommGroup N] [AddCommMonoid P] [Module R N] [Module R M]
    [Module R P] (f : M →ₗ[R] N) :
    Function.Exact (0 : P →ₗ[R] M) f ↔ Function.Injective f

Proof state:
R : Type u_8
inst✝⁶ : Ring R
M : Type u_12
N : Type u_13
P : Type u_14
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommMonoid P
inst✝² : Module R N
inst✝¹ : Module R M
inst✝ : Module R P
f : M →ₗ[R] N
⊢ Exact ⇑0 ⇑f ↔ Injective ⇑f

Tactic:
simp [← ker_eq_bot, exact_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_setIfInBounds_ne (as : Array α) {i : Nat} (v : α) {j : Nat}
    (hj : j < (as.setIfInBounds i v).size) (h : i ≠ j) :
    (as.setIfInBounds i v)[j]'hj = as[j]'(by simpa using hj)

Proof state:
α : Type u_1
as : Array α
i : Nat
v : α
j : Nat
hj : j < (as.setIfInBounds i v).size
h : i ≠ j
⊢ (as.setIfInBounds i v)[j] = as[j]

Tactic:
simp [getElem_setIfInBounds, h]

Result:
no goals

Proof state:
α : Type ?u.133555
as : Array α
i : Nat
v : α
j : Nat
hj : j < (as.setIfInBounds i v).size
h : i ≠ j
⊢ j < as.size

Tactic:
simpa using hj

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_eq_zero {a : R[X]} : a.toFinsupp = 0 ↔ a = 0

Proof state:
R : Type u
inst✝ : Semiring R
a : R[X]
⊢ a.toFinsupp = 0 ↔ a = 0

Tactic:
rw [← toFinsupp_zero, toFinsupp_inj]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem map_inv (I : FractionalIdeal R₁⁰ K) (h : K ≃ₐ[R₁] K') :
    I⁻¹.map (h : K →ₐ[R₁] K') = (I.map h)⁻¹

Proof state:
K : Type u_3
inst✝⁷ : Field K
R₁ : Type u_4
inst✝⁶ : CommRing R₁
inst✝⁵ : IsDomain R₁
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) I⁻¹ = (map (↑h) I)⁻¹

Tactic:
rw [inv_eq, map_div, map_one, inv_eq]

Result:
no goals