harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Except.lean
theorem map_id : Except.map (ε := ε) (α := α) (β := α) id = id

Proof state:
case h
ε : Type u
α : Type u_1
⊢ ∀ (x : Except ε α), Except.map id x = id x

Tactic:
intro e

Result:
case h
ε : Type u
α : Type u_1
e : Except ε α
⊢ Except.map id e = id e

Proof state:
case h
ε : Type u
α : Type u_1
e : Except ε α
⊢ Except.map id e = id e

Tactic:
simp [Except.map]

Result:
case h
ε : Type u
α : Type u_1
e : Except ε α
⊢ (match e with
    | error err => error err
    | ok v => ok v) =
    e

Proof state:
case h
ε : Type u
α : Type u_1
e : Except ε α
⊢ (match e with
    | error err => error err
    | ok v => ok v) =
    e

Tactic:
cases e <;> rfl

Result:
no goals

Proof state:
ε : Type u
α : Type u_1
⊢ Except.map id = id

Tactic:
apply funext

Result:
case h
ε : Type u
α : Type u_1
⊢ ∀ (x : Except ε α), Except.map id x = id x
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma hurwitzZetaEven_residue_one (a : UnitAddCircle) :
    Tendsto (fun s ↦ (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Proof state:
a : UnitAddCircle
this : Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
⊢ Tendsto (fun s => (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
refine this.congr' ?_

Result:
a : UnitAddCircle
this : Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
⊢ (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) =ᶠ[𝓝[≠] 1] fun s => (s - 1) * hurwitzZetaEven a s

Proof state:
a : UnitAddCircle
⊢ Tendsto (fun s => (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
have : Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s / Gammaℝ s) (𝓝[≠] 1) (𝓝 1) := by
  simpa only [Gammaℝ_one, inv_one, mul_one] using (completedHurwitzZetaEven_residue_one a).mul
    <| (differentiable_Gammaℝ_inv.continuous.tendsto _).mono_left nhdsWithin_le_nhds

Result:
a : UnitAddCircle
this : Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
⊢ Tendsto (fun s => (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Proof state:
a : UnitAddCircle
this : Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
⊢ (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) =ᶠ[𝓝[≠] 1] fun s => (s - 1) * hurwitzZetaEven a s

Tactic:
filter_upwards [eventually_ne_nhdsWithin one_ne_zero] with s hs

Result:
case h
a : UnitAddCircle
this : Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
s : ℂ
hs : s ≠ 0
⊢ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ = (s - 1) * hurwitzZetaEven a s

Proof state:
case h
a : UnitAddCircle
this : Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
s : ℂ
hs : s ≠ 0
⊢ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ = (s - 1) * hurwitzZetaEven a s

Tactic:
simp [hurwitzZetaEven_def_of_ne_or_ne (Or.inr hs), mul_div_assoc]

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)

Tactic:
simpa only [Gammaℝ_one, inv_one, mul_one] using (completedHurwitzZetaEven_residue_one a).mul
  <| (differentiable_Gammaℝ_inv.continuous.tendsto _).mono_left nhdsWithin_le_nhds

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma disjoint_genWeightSpace [NoZeroSMulDivisors R M] {χ₁ χ₂ : L → R} (h : χ₁ ≠ χ₂) :
    Disjoint (genWeightSpace M χ₁) (genWeightSpace M χ₂)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
χ₁ χ₂ : L → R
h : χ₁ ≠ χ₂
⊢ Disjoint (genWeightSpace M χ₁) (genWeightSpace M χ₂)

Tactic:
obtain ⟨x, hx⟩ : ∃ x, χ₁ x ≠ χ₂ x := Function.ne_iff.mp h

Result:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
χ₁ χ₂ : L → R
h : χ₁ ≠ χ₂
x : L
hx : χ₁ x ≠ χ₂ x
⊢ Disjoint (genWeightSpace M χ₁) (genWeightSpace M χ₂)

Proof state:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
χ₁ χ₂ : L → R
h : χ₁ ≠ χ₂
x : L
hx : χ₁ x ≠ χ₂ x
⊢ Disjoint (genWeightSpace M χ₁) (genWeightSpace M χ₂)

Tactic:
exact (disjoint_genWeightSpaceOf R L M hx).mono
  (genWeightSpace_le_genWeightSpaceOf M x χ₁) (genWeightSpace_le_genWeightSpaceOf M x χ₂)

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem lt_card_le_iff_apply_le_of_monotone [PartialOrder α] [DecidableRel (α := α) LE.le]
    {m : ℕ} (f : Fin m → α) (a : α) (h_sorted : Monotone f) (j : Fin m) :
    j < Fintype.card {i // f i ≤ a} ↔ f j ≤ a

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
hc : Fintype.card { i // f i ≤ a } ≤ ↑j
p : Fin m → Prop := fun x => f x ≤ a
q : Fin m → Prop := fun x => ↑x < Fintype.card { i // f i ≤ a }
q' : { i // f i ≤ a } → Prop := fun x => q ↑x
hw : 0 < Fintype.card { j // ¬q' j }
he : Fintype.card ({ a // q' a } ⊕ { a // ¬q' a }) = Fintype.card { i // f i ≤ a }
h4 : Fintype.card { x // q ↑x } = Fintype.card (Subtype q)
h_le : Fintype.card { i // f i ≤ a } ≤ m
⊢ Fintype.card { j // ¬q' j } = 0

Tactic:
rwa [Fintype.card_sum, h4, Fintype.card_fin_lt_of_le h_le, add_right_eq_self] at he

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
⊢ ↑j < Fintype.card { i // f i ≤ a }

Tactic:
by_contra! hc

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
hc : Fintype.card { i // f i ≤ a } ≤ ↑j
⊢ False
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
@[simp]
lemma ofBijectiveAlgebraMap_jacobian (h : Function.Bijective (algebraMap R S)) :
    (ofBijectiveAlgebraMap h).jacobian = 1

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
⊢ (ofBijectiveAlgebraMap h).jacobian = 1

Tactic:
have : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix
    (ofBijectiveAlgebraMap h).jacobiMatrix = 1 := by
  ext (i j : PEmpty)
  contradiction

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
this : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix = 1
⊢ (ofBijectiveAlgebraMap h).jacobian = 1

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
⊢ (ofBijectiveAlgebraMap h).jacobian = 1

Tactic:
classical
have : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix
    (ofBijectiveAlgebraMap h).jacobiMatrix = 1 := by
  ext (i j : PEmpty)
  contradiction
rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]

Result:
no goals

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
i j : PEmpty.{?u.47196 + 1}
⊢ (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix i j = 1 i j

Tactic:
contradiction

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
⊢ (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix = 1

Tactic:
ext (i j : PEmpty)

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
i j : PEmpty.{?u.47196 + 1}
⊢ (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix i j = 1 i j

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
this : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix = 1
⊢ (ofBijectiveAlgebraMap h).jacobian = 1

Tactic:
rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Nontrivial.infsep_lt_iff {d} (hs : s.Nontrivial) :
    s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y

Tactic:
exact hs.le_infsep_iff

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d

Tactic:
rw [← not_iff_not]

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ ¬s.infsep < d ↔ ¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ ¬s.infsep < d ↔ ¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d

Tactic:
push_neg

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_le_iff_le_log' {b x c : Ordinal} (hb : 1 < b) (hc : c ≠ 0) :
    b ^ c ≤ x ↔ c ≤ log b x

Proof state:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b = 0 ∧ c ≠ 0 ↔ c = 0

Tactic:
simp [hc, (zero_lt_one.trans hb).ne']

Result:
no goals

Proof state:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ 0 ↔ c ≤ log b 0

Tactic:
rw [log_zero_right, Ordinal.le_zero, Ordinal.le_zero, opow_eq_zero]

Result:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b = 0 ∧ c ≠ 0 ↔ c = 0

Proof state:
case inr
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
hx : x ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
exact opow_le_iff_le_log hb hx

Result:
no goals

Proof state:
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ 0 ↔ c ≤ log b 0

case inr
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
hx : x ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x
-- Mathlib/GroupTheory/Sylow.lean
theorem card_eq_multiplicity [Finite G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G) :
    Nat.card P = p ^ Nat.factorization (Nat.card G) p

Proof state:
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card ↥↑P = p ^ n
⊢ Nat.card ↥↑P ∣ Nat.card G

Tactic:
exact P.1.card_subgroup_dvd_card

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
⊢ Nat.card ↥↑P = p ^ (Nat.card G).factorization p

Tactic:
obtain ⟨n, heq : Nat.card P = _⟩ := IsPGroup.iff_card.mp P.isPGroup'

Result:
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card ↥↑P = p ^ n
⊢ Nat.card ↥↑P = p ^ (Nat.card G).factorization p

Proof state:
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card ↥↑P = p ^ n
⊢ Nat.card ↥↑P = p ^ (Nat.card G).factorization p

Tactic:
refine Nat.dvd_antisymm ?_ (P.pow_dvd_card_of_pow_dvd_card (Nat.ordProj_dvd _ p))

Result:
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card ↥↑P = p ^ n
⊢ Nat.card ↥↑P ∣ p ^ (Nat.card G).factorization p

Proof state:
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card ↥↑P = p ^ n
⊢ Nat.card ↥↑P ∣ p ^ (Nat.card G).factorization p

Tactic:
rw [heq, ← hp.out.pow_dvd_iff_dvd_ordProj (show Nat.card G ≠ 0 from Nat.card_pos.ne'), ← heq]

Result:
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card ↥↑P = p ^ n
⊢ Nat.card ↥↑P ∣ Nat.card G
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigO.comp_fst : f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
simp only [isBigO_iff, eventually_prod_iff]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∃ c pa,
      (∀ᶠ (x : α) in l, pa x) ∧
        ∃ pb,
          (∀ᶠ (y : β) in l', pb y) ∧
            ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∃ c pa,
      (∀ᶠ (x : α) in l, pa x) ∧
        ∃ pb,
          (∀ᶠ (y : β) in l', pb y) ∧
            ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖

Tactic:
exact fun ⟨c, hc⟩ ↦ ⟨c, _, hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩

Result:
no goals
-- Mathlib/Data/Nat/BitIndices.lean
theorem bitIndices_two_pow_mul (k n : ℕ) :
    bitIndices (2^k * n) = (bitIndices n).map (· + k)

Proof state:
case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x => x + k) n.bitIndices
⊢ map (fun x => x + (k + 1)) n.bitIndices = map (fun x => x + (1 + k)) n.bitIndices

Tactic:
simp [add_comm (a := 1)]

Result:
no goals

Proof state:
case zero
n : ℕ
⊢ (2 ^ 0 * n).bitIndices = map (fun x => x + 0) n.bitIndices

Tactic:
simp

Result:
no goals

Proof state:
case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x => x + k) n.bitIndices
⊢ (2 ^ (k + 1) * n).bitIndices = map (fun x => x + (k + 1)) n.bitIndices

Tactic:
rw [add_comm, pow_add, pow_one, mul_assoc, bitIndices_two_mul, ih, List.map_map, comp_add_right]

Result:
case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x => x + k) n.bitIndices
⊢ map (fun x => x + (k + 1)) n.bitIndices = map (fun x => x + (1 + k)) n.bitIndices

Proof state:
k n : ℕ
⊢ (2 ^ k * n).bitIndices = map (fun x => x + k) n.bitIndices

Tactic:
induction' k with k ih

Result:
case zero
n : ℕ
⊢ (2 ^ 0 * n).bitIndices = map (fun x => x + 0) n.bitIndices

case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x => x + k) n.bitIndices
⊢ (2 ^ (k + 1) * n).bitIndices = map (fun x => x + (k + 1)) n.bitIndices
-- Mathlib/Order/Filter/Map.lean
theorem map_biInf_eq {ι : Type w} {f : ι → Filter α} {m : α → β} {p : ι → Prop}
    (h : DirectedOn (f ⁻¹'o (· ≥ ·)) { x | p x }) (ne : ∃ i, p i) :
    map m (⨅ (i) (_ : p i), f i) = ⨅ (i) (_ : p i), map m (f i)

Proof state:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) {x | p x}
ne : ∃ i, p i
⊢ map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), map m (f i)

Tactic:
haveI := nonempty_subtype.2 ne

Result:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) {x | p x}
ne : ∃ i, p i
this : Nonempty (Subtype p)
⊢ map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), map m (f i)

Proof state:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) {x | p x}
ne : ∃ i, p i
this : Nonempty (Subtype p)
⊢ map m (⨅ x, f ↑x) = ⨅ x, map m (f ↑x)

Tactic:
exact map_iInf_eq h.directed_val

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) {x | p x}
ne : ∃ i, p i
this : Nonempty (Subtype p)
⊢ map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), map m (f i)

Tactic:
simp only [iInf_subtype']

Result:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) {x | p x}
ne : ∃ i, p i
this : Nonempty (Subtype p)
⊢ map m (⨅ x, f ↑x) = ⨅ x, map m (f ↑x)
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
/-- The composition of a primitive additive character with an injective mooid homomorphism
is also primitive. -/
lemma IsPrimitive.compMulHom_of_isPrimitive {R'' : Type*} [CommMonoid R''] {φ : AddChar R R'}
    {f : R' →* R''} (hφ : φ.IsPrimitive) (hf : Function.Injective f) :
    (f.compAddChar φ).IsPrimitive := fun a ha ↦ by
  simpa [DFunLike.ext_iff] using (MonoidHom.compAddChar_injective_right f hf).ne (hφ ha)

Proof state:
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
R'' : Type u_1
inst✝ : CommMonoid R''
φ : AddChar R R'
f : R' →* R''
hφ : φ.IsPrimitive
hf : Function.Injective ⇑f
a : R
ha : a ≠ 0
⊢ (f.compAddChar φ).mulShift a ≠ 1

Tactic:
simpa [DFunLike.ext_iff] using (MonoidHom.compAddChar_injective_right f hf).ne (hφ ha)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_eq (hs : MeasurableSet s) : ae (μ.restrict s) = ae μ ⊓ 𝓟 s

Proof state:
case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ (tᶜ ∩ s) = 0 ↔ μ {a | a ∉ t ∧ a ∈ s} = 0

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ae (μ.restrict s) = ae μ ⊓ 𝓟 s

Tactic:
ext t

Result:
case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ t ∈ ae (μ.restrict s) ↔ t ∈ ae μ ⊓ 𝓟 s

Proof state:
case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ t ∈ ae (μ.restrict s) ↔ t ∈ ae μ ⊓ 𝓟 s

Tactic:
simp only [mem_inf_principal, mem_ae_iff, restrict_apply_eq_zero' hs, compl_setOf,
  Classical.not_imp, fun a => and_comm (a := a ∈ s) (b := ¬a ∈ t)]

Result:
case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ (tᶜ ∩ s) = 0 ↔ μ {a | a ∉ t ∧ a ∈ s} = 0
-- Mathlib/Data/Multiset/Dedup.lean
theorem Subset.dedup_add_right {s t : Multiset α} (h : s ⊆ t) :
    dedup (s + t) = dedup t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ (s + t).dedup = t.dedup

Tactic:
induction s, t using Quot.induction_on₂

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ (Quot.mk (⇑(isSetoid α)) a✝ + Quot.mk (⇑(isSetoid α)) b✝).dedup = dedup (Quot.mk (⇑(isSetoid α)) b✝)

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ (Quot.mk (⇑(isSetoid α)) a✝ + Quot.mk (⇑(isSetoid α)) b✝).dedup = dedup (Quot.mk (⇑(isSetoid α)) b✝)

Tactic:
exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.dedup_append_right h

Result:
no goals
-- Mathlib/RingTheory/Valuation/Integers.lean
theorem le_of_dvd (hv : Integers v O) {x y : O} (h : x ∣ y) :
    v (algebraMap O R y) ≤ v (algebraMap O R x)

Proof state:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ v ((algebraMap O R) x) * v ((algebraMap O R) z) ≤ v ((algebraMap O R) x) * 1

Tactic:
exact mul_le_mul_left' (hv.2 z) _

Result:
no goals

Proof state:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x y : O
h : x ∣ y
⊢ v ((algebraMap O R) y) ≤ v ((algebraMap O R) x)

Tactic:
let ⟨z, hz⟩ := h

Result:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ v ((algebraMap O R) y) ≤ v ((algebraMap O R) x)

Proof state:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ v ((algebraMap O R) y) ≤ v ((algebraMap O R) x)

Tactic:
rw [← mul_one (v (algebraMap O R x)), hz, RingHom.map_mul, v.map_mul]

Result:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ v ((algebraMap O R) x) * v ((algebraMap O R) z) ≤ v ((algebraMap O R) x) * 1
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem adjoin_minpoly_coeff_of_exists_primitive_element
    [FiniteDimensional F E] (hprim : adjoin F {α} = ⊤) (K : IntermediateField F E) :
    adjoin F ((minpoly K α).map (algebraMap K E)).coeffs = K

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree
⊢ K' = K

Tactic:
refine eq_of_le_of_finrank_le' hsub ?_

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree
⊢ finrank (↥K') E ≤ finrank (↥K) E