harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem pow_div_two_eq_neg_one_or_one {a : ZMod p} (ha : a ≠ 0) :
    a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1

Proof state:
case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
⊢ a ≠ 0 → a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

Tactic:
fin_cases a

Result:
case inl.«0»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i => i) ⟨0, ⋯⟩ ≠ 0 → (fun i => i) ⟨0, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i => i) ⟨0, ⋯⟩ ^ (2 / 2) = -1

case inl.«1»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i => i) ⟨1, ⋯⟩ ≠ 0 → (fun i => i) ⟨1, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i => i) ⟨1, ⋯⟩ ^ (2 / 2) = -1

Proof state:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p - 1) = 1

Tactic:
exact pow_card_sub_one_eq_one ha

Result:
no goals

Proof state:
case inl
inst✝ : Fact (Nat.Prime 2)
⊢ ∀ {a : ZMod 2}, a ≠ 0 → a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

Tactic:
intro a

Result:
case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
⊢ a ≠ 0 → a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

Proof state:
case inl.«0»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i => i) ⟨0, ⋯⟩ ≠ 0 → (fun i => i) ⟨0, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i => i) ⟨0, ⋯⟩ ^ (2 / 2) = -1

Tactic:
tauto

Result:
no goals

Proof state:
case inl.«1»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i => i) ⟨1, ⋯⟩ ≠ 0 → (fun i => i) ⟨1, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i => i) ⟨1, ⋯⟩ ^ (2 / 2) = -1

Tactic:
simp

Result:
no goals

Proof state:
case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
ha : a ≠ 0
⊢ a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

Tactic:
revert a ha

Result:
case inl
inst✝ : Fact (Nat.Prime 2)
⊢ ∀ {a : ZMod 2}, a ≠ 0 → a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

Proof state:
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp2 : p = 2
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1

Tactic:
subst p

Result:
case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
ha : a ≠ 0
⊢ a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1

Tactic:
rcases Prime.eq_two_or_odd (@Fact.out p.Prime _) with hp2 | hp_odd

Result:
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp2 : p = 2
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1

case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1

Proof state:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1

Tactic:
rw [← mul_self_eq_one_iff, ← pow_add, ← two_mul, two_mul_odd_div_two hp_odd]

Result:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p - 1) = 1
-- Mathlib/Combinatorics/Quiver/Push.lean
theorem lift_comp : (of σ ⋙q lift σ φ τ h) = φ

Proof state:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (lift σ φ τ h).obj ((of σ).obj X) = φ.obj X

Tactic:
apply Eq.symm

Result:
case h_obj.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ φ.obj X = (lift σ φ τ h).obj ((of σ).obj X)

Proof state:
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (⋯ ▸ ⋯ ▸ φ.map f) (φ.map f)

Tactic:
apply (eqRec_heq _ _).trans

Result:
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (⋯ ▸ φ.map f) (φ.map f)
-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_apply_eq_top' (s_mble : MeasurableSet s) : count s = ∞ ↔ s.Infinite

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : s.Finite
⊢ count s = ⊤ ↔ s.Infinite

Tactic:
simp [Set.Infinite, hs, count_apply_finite' hs s_mble]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
⊢ count s = ⊤ ↔ s.Infinite

Tactic:
by_cases hs : s.Finite

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : s.Finite
⊢ count s = ⊤ ↔ s.Infinite

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : ¬s.Finite
⊢ count s = ⊤ ↔ s.Infinite

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : s.Infinite
⊢ count s = ⊤ ↔ s.Infinite

Tactic:
simp [hs, count_apply_infinite]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : ¬s.Finite
⊢ count s = ⊤ ↔ s.Infinite

Tactic:
change s.Infinite at hs

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : s.Infinite
⊢ count s = ⊤ ↔ s.Infinite
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_const (q : ℚ) : norm (const (padicNorm p) q) = padicNorm p q

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ norm (const (padicNorm p) q) = padicNorm p q

Tactic:
obtain rfl | hq := eq_or_ne q 0

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm (const (padicNorm p) 0) = padicNorm p 0

case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q

Tactic:
simp [norm, not_equiv_zero_const_of_nonzero hq]

Result:
no goals

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm (const (padicNorm p) 0) = padicNorm p 0

Tactic:
simp [norm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem tendsto_pre_nat (m : Set X → ℝ≥0∞) (s : Set X) :
    Tendsto (fun n : ℕ => pre m n⁻¹ s) atTop (𝓝 <| mkMetric' m s)

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓟 (Ioi 0))

Tactic:
refine tendsto_principal.2 (Eventually.of_forall fun n => ?_)

Result:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
n : ℕ
⊢ (↑n)⁻¹ ∈ Ioi 0

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun n => (pre m (↑n)⁻¹) s) atTop (𝓝 ((mkMetric' m) s))

Tactic:
refine (tendsto_pre m s).comp (tendsto_inf.2 ⟨ENNReal.tendsto_inv_nat_nhds_zero, ?_⟩)

Result:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓟 (Ioi 0))

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
n : ℕ
⊢ (↑n)⁻¹ ∈ Ioi 0

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive]
lemma orbitRel.quotient_eq_of_quotient_subgroup_eq {H : Subgroup G} {a b : α}
    (h : (⟦a⟧ : orbitRel.Quotient H α) = ⟦b⟧) : (⟦a⟧ : orbitRel.Quotient G α) = ⟦b⟧

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
a b : α
h : (orbitRel (↥H) α) a b
⊢ (orbitRel G α) a b

Tactic:
exact mem_orbit_of_mem_orbit_subgroup h

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
a b : α
h : ⟦a⟧ = ⟦b⟧
⊢ ⟦a⟧ = ⟦b⟧

Tactic:
rw [@Quotient.eq] at h ⊢

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
a b : α
h : (orbitRel (↥H) α) a b
⊢ (orbitRel G α) a b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_eq_iff : map f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map f

Proof state:
case mk
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l' : Array α✝
toList✝ : List α✝¹
⊢ map f { toList := toList✝ } = l' ↔ ∀ (i : Nat), l'[i]? = Option.map f { toList := toList✝ }[i]?

Tactic:
cases l'

Result:
case mk.mk
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
toList✝¹ : List α✝¹
toList✝ : List α✝
⊢ map f { toList := toList✝¹ } = { toList := toList✝ } ↔
    ∀ (i : Nat), { toList := toList✝ }[i]? = Option.map f { toList := toList✝¹ }[i]?

Proof state:
case mk.mk
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
toList✝¹ : List α✝¹
toList✝ : List α✝
⊢ map f { toList := toList✝¹ } = { toList := toList✝ } ↔
    ∀ (i : Nat), { toList := toList✝ }[i]? = Option.map f { toList := toList✝¹ }[i]?

Tactic:
simp [List.map_eq_iff]

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : Array α✝¹
l' : Array α✝
⊢ map f l = l' ↔ ∀ (i : Nat), l'[i]? = Option.map f l[i]?

Tactic:
cases l

Result:
case mk
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l' : Array α✝
toList✝ : List α✝¹
⊢ map f { toList := toList✝ } = l' ↔ ∀ (i : Nat), l'[i]? = Option.map f { toList := toList✝ }[i]?
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
lemma deriv_aeval_eq_implicitDeriv (x : R) (v : A[X]) (h : x′ = aeval x v) (p : A[X]) :
    (aeval x p)′ = aeval x (implicitDeriv v p)

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
v : A[X]
h : x′ = (aeval x) v
p : A[X]
⊢ ((aeval x) p)′ = (aeval x) ((implicitDeriv v) p)

Tactic:
simp [deriv_aeval_eq, implicitDeriv, h, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem Pairwise.rel_of_mem_append
    {l₁ l₂ : List α} (h : (l₁ ++ l₂).Pairwise R) (hx : x ∈ l₁) (hy : y ∈ l₂) : R x y

Proof state:
α : Type u_1
R : α → α → Prop
x y : α
l₁ l₂ : List α
h : Pairwise R (l₁ ++ l₂)
hx : x ∈ l₁
hy : y ∈ l₂
⊢ [x] <+ l₁

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
x y : α
l₁ l₂ : List α
h : Pairwise R (l₁ ++ l₂)
hx : x ∈ l₁
hy : y ∈ l₂
⊢ R x y

Tactic:
apply pairwise_iff_forall_sublist.mp h

Result:
α : Type u_1
R : α → α → Prop
x y : α
l₁ l₂ : List α
h : Pairwise R (l₁ ++ l₂)
hx : x ∈ l₁
hy : y ∈ l₂
⊢ [x, y] <+ l₁ ++ l₂

Proof state:
α : Type u_1
R : α → α → Prop
x y : α
l₁ l₂ : List α
h : Pairwise R (l₁ ++ l₂)
hx : x ∈ l₁
hy : y ∈ l₂
⊢ ∃ l₁_1 l₂_1, [x, y] = l₁_1 ++ l₂_1 ∧ l₁_1 <+ l₁ ∧ l₂_1 <+ l₂

Tactic:
exact ⟨[x], [y], rfl, by simpa, by simpa⟩

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
x y : α
l₁ l₂ : List α
h : Pairwise R (l₁ ++ l₂)
hx : x ∈ l₁
hy : y ∈ l₂
⊢ [x, y] <+ l₁ ++ l₂

Tactic:
rw [sublist_append_iff]

Result:
α : Type u_1
R : α → α → Prop
x y : α
l₁ l₂ : List α
h : Pairwise R (l₁ ++ l₂)
hx : x ∈ l₁
hy : y ∈ l₂
⊢ ∃ l₁_1 l₂_1, [x, y] = l₁_1 ++ l₂_1 ∧ l₁_1 <+ l₁ ∧ l₂_1 <+ l₂

Proof state:
α : Type u_1
R : α → α → Prop
x y : α
l₁ l₂ : List α
h : Pairwise R (l₁ ++ l₂)
hx : x ∈ l₁
hy : y ∈ l₂
⊢ [y] <+ l₂

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem findSome?_eq_none_iff {f : Fin n → Option α} :
    findSome? f = none ↔ ∀ i, f i = none

Proof state:
case mpr
n : Nat
α : Type u_1
f : Fin n → Option α
hf : ∀ (i : Fin n), f i = none
⊢ findSome? f = none

Tactic:
match h : findSome? f with
| none => rfl
| some x =>
  match exists_of_findSome?_eq_some h with
  | ⟨i, h⟩ => rw [hf] at h; contradiction

Result:
no goals

Proof state:
case mpr
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ (∀ (i : Fin n), f i = none) → findSome? f = none

Tactic:
intro hf

Result:
case mpr
n : Nat
α : Type u_1
f : Fin n → Option α
hf : ∀ (i : Fin n), f i = none
⊢ findSome? f = none

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
hf : ∀ (i : Fin n), f i = none
x : α
h✝ : findSome? f = some x
i : Fin n
h : none = some x
⊢ some x = none

Tactic:
contradiction

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ findSome? f = none ↔ ∀ (i : Fin n), f i = none

Tactic:
constructor

Result:
case mp
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ findSome? f = none → ∀ (i : Fin n), f i = none

case mpr
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ (∀ (i : Fin n), f i = none) → findSome? f = none

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
hf : ∀ (i : Fin n), f i = none
h : findSome? f = none
⊢ none = none

Tactic:
rfl

Result:
no goals

Proof state:
case mp
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ findSome? f = none → ∀ (i : Fin n), f i = none

Tactic:
exact eq_none_of_findSome?_eq_none

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
hf : ∀ (i : Fin n), f i = none
x : α
h : findSome? f = some x
⊢ some x = none

Tactic:
match exists_of_findSome?_eq_some h with
| ⟨i, h⟩ => rw [hf] at h; contradiction

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
hf : ∀ (i : Fin n), f i = none
x : α
h✝ : findSome? f = some x
i : Fin n
h : f i = some x
⊢ some x = none

Tactic:
rw [hf] at h

Result:
n : Nat
α : Type u_1
f : Fin n → Option α
hf : ∀ (i : Fin n), f i = none
x : α
h✝ : findSome? f = some x
i : Fin n
h : none = some x
⊢ some x = none
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
lemma algHom_deriv (f : R →ₐ[A] R') (hf : Function.Injective f) (x : R) (h : IsSeparable A x) :
    f (x′) = (f x)′

Proof state:
case ha
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ (f.comp (aeval x)) (derivative p) ≠ 0

Tactic:
simp only [AlgHom.coe_comp, Function.comp_apply, ne_eq, map_eq_zero_iff f hf]

Result:
case ha
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ ¬(aeval x) (derivative p) = 0

Proof state:
case ha
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ (aeval (f x)) (derivative p) ≠ 0

Tactic:
rw [Polynomial.aeval_algHom]

Result:
case ha
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ (f.comp (aeval x)) (derivative p) ≠ 0

Proof state:
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
⊢ f x′ = (f x)′

Tactic:
let p := minpoly A x

Result:
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ f x′ = (f x)′
-- Mathlib/Order/Monotone/MonovaryOrder.lean
lemma monovary_iff_exists_monotone :
    Monovary f g ↔ ∃ (_ : LinearOrder ι), Monotone f ∧ Monotone g

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
⊢ Monovary f g ↔ ∃ x, Monotone f ∧ Monotone g

Tactic:
simp [← monovaryOn_univ, monovaryOn_iff_exists_monotoneOn]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem spanExt_inv_app_left : (spanExt iX iY iZ wf wg).inv.app WalkingSpan.left = iY.inv

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 ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).inv.app WalkingSpan.left = iY.inv

Tactic:
dsimp [spanExt]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem Multiset.aemeasurable_prod' (l : Multiset (α → M)) (hl : ∀ f ∈ l, AEMeasurable f μ) :
    AEMeasurable l.prod μ

Proof state:
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : Multiset (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
⊢ AEMeasurable l.prod μ

Tactic:
rcases l with ⟨l⟩

Result:
case mk
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, AEMeasurable f μ
⊢ AEMeasurable (prod (Quot.mk (⇑(List.isSetoid (α → M))) l)) μ

Proof state:
case mk
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, AEMeasurable f μ
⊢ AEMeasurable (prod (Quot.mk (⇑(List.isSetoid (α → M))) l)) μ

Tactic:
simpa using l.aemeasurable_prod' (by simpa using hl)

Result:
no goals

Proof state:
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, AEMeasurable f μ
⊢ ∀ f ∈ l, AEMeasurable f μ

Tactic:
simpa using hl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem map_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → δ a} :
    m.map f = Raw₀.map f ⟨m, h.size_buckets_pos⟩

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
f : (a : α) → β a → δ a
⊢ Raw.map f m = (Raw₀.map f ⟨m, ⋯⟩).val

Tactic:
simp [Raw.map, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem Equiv.induced_symm {α β : Type*} (e : α ≃ β) :
    TopologicalSpace.induced e.symm = TopologicalSpace.coinduced e

Proof state:
case h.a.h.a
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ IsOpen U ↔ IsOpen U

Tactic:
rw [isOpen_induced_iff, isOpen_coinduced]

Result:
case h.a.h.a
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ (∃ t_1, IsOpen t_1 ∧ ⇑e.symm ⁻¹' t_1 = U) ↔ IsOpen (⇑e ⁻¹' U)

Proof state:
α : Type u_4
β : Type u_5
e : α ≃ β
⊢ TopologicalSpace.induced ⇑e.symm = TopologicalSpace.coinduced ⇑e

Tactic:
ext t U

Result:
case h.a.h.a
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ IsOpen U ↔ IsOpen U

Proof state:
case h.a.h.a
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ (∃ t_1, IsOpen t_1 ∧ ⇑e.symm ⁻¹' t_1 = U) ↔ IsOpen (⇑e ⁻¹' U)

Tactic:
simp only [e.symm.preimage_eq_iff_eq_image, exists_eq_right, ← preimage_equiv_eq_image_symm]

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem addVal_def (r : R) (u : Rˣ) {ϖ : R} (hϖ : Irreducible ϖ) (n : ℕ) (hr : r = u * ϖ ^ n) :
    addVal R r = n

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
r : R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
hr : r = ↑u * ϖ ^ n
⊢ (addVal R) r = ↑n

Tactic:
classical
rw [addVal, multiplicity_addValuation_apply, hr, emultiplicity_eq_of_associated_left
    (associated_of_irreducible R hϖ (Classical.choose_spec (exists_prime R)).irreducible),
  emultiplicity_eq_of_associated_right (Associated.symm ⟨u, mul_comm _ _⟩),
  emultiplicity_pow_self_of_prime (irreducible_iff_prime.1 hϖ)]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
r : R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
hr : r = ↑u * ϖ ^ n
⊢ (addVal R) r = ↑n

Tactic:
rw [addVal, multiplicity_addValuation_apply, hr, emultiplicity_eq_of_associated_left
    (associated_of_irreducible R hϖ (Classical.choose_spec (exists_prime R)).irreducible),
  emultiplicity_eq_of_associated_right (Associated.symm ⟨u, mul_comm _ _⟩),
  emultiplicity_pow_self_of_prime (irreducible_iff_prime.1 hϖ)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Bitwise.lean
theorem Bool.toBitVec_toUSize {b : Bool} :
    b.toUSize.toBitVec = (BitVec.ofBool b).setWidth System.Platform.numBits

Proof state:
case true.a

⊢ true.toUSize.toBitVec.toNat = (BitVec.setWidth System.Platform.numBits (BitVec.ofBool true)).toNat

Tactic:
simp [toUSize]

Result:
no goals

Proof state:
case false

⊢ false.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool false)

Tactic:
simp [toUSize]

Result:
no goals

Proof state:
case true

⊢ true.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool true)

Tactic:
apply BitVec.eq_of_toNat_eq

Result:
case true.a

⊢ true.toUSize.toBitVec.toNat = (BitVec.setWidth System.Platform.numBits (BitVec.ofBool true)).toNat

Proof state:
b : Bool
⊢ b.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool b)

Tactic:
cases b

Result:
case false

⊢ false.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool false)

case true

⊢ true.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool true)
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem summable_sigma {β : α → Type*} {f : (Σ x, β x) → ℝ≥0} :
    Summable f ↔ (∀ x, Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' y, f ⟨x, y⟩

Proof state:
case mp
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ (Summable fun a => ↑(f a)) →
    (∀ (x : α), Summable fun a => ↑(f ⟨x, a⟩)) ∧ Summable fun a => ∑' (a_1 : β a), ↑(f ⟨a, a_1⟩)

Tactic:
exact fun h => ⟨h.sigma_factor, h.sigma⟩

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
h₁ : ∀ (x : α), Summable fun y => f ⟨x, y⟩
h₂ : Summable fun x => ∑' (y : β x), f ⟨x, y⟩
⊢ Summable f

Tactic:
simpa only [← ENNReal.tsum_coe_ne_top_iff_summable, ENNReal.tsum_sigma',
  ENNReal.coe_tsum (h₁ _)] using h₂

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ ((∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩) → Summable f

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mpr.intro
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
h₁ : ∀ (x : α), Summable fun y => f ⟨x, y⟩
h₂ : Summable fun x => ∑' (y : β x), f ⟨x, y⟩
⊢ Summable f

Proof state:
case mp
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ Summable f → (∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩

Tactic:
simp only [← NNReal.summable_coe, NNReal.coe_tsum]

Result:
case mp
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ (Summable fun a => ↑(f a)) →
    (∀ (x : α), Summable fun a => ↑(f ⟨x, a⟩)) ∧ Summable fun a => ∑' (a_1 : β a), ↑(f ⟨a, a_1⟩)

Proof state:
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ Summable f ↔ (∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩

Tactic:
constructor

Result:
case mp
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ Summable f → (∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩

case mpr
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ ((∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩) → Summable f