harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem prev_nat_zero : (ComplexShape.up ℕ).prev 0 = 0

Proof state:
i✝ : ℕ
⊢ ¬(ComplexShape.up ℕ).Rel i✝ 0

Tactic:
apply Nat.noConfusion

Result:
no goals

Proof state:
⊢ ∀ (i : ℕ), ¬(ComplexShape.up ℕ).Rel i 0

Tactic:
intro

Result:
i✝ : ℕ
⊢ ¬(ComplexShape.up ℕ).Rel i✝ 0

Proof state:
⊢ ¬∃ i, (ComplexShape.up ℕ).Rel i 0

Tactic:
push_neg

Result:
⊢ ∀ (i : ℕ), ¬(ComplexShape.up ℕ).Rel i 0

Proof state:
⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
classical
  refine dif_neg ?_
  push_neg
  intro
  apply Nat.noConfusion

Result:
no goals

Proof state:
⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
refine dif_neg ?_

Result:
⊢ ¬∃ i, (ComplexShape.up ℕ).Rel i 0
-- Mathlib/Logic/Embedding/Set.lean
theorem Function.Embedding.sumSet_preimage_inr (h : Disjoint s t) :
    .inr ⁻¹' (Function.Embedding.sumSet h ⁻¹' r) = r ∩ t

Proof state:
α : Type u_1
s t r : Set α
h : Disjoint s t
⊢ Subtype.val '' (Sum.inr ⁻¹' (⇑(sumSet h) ⁻¹' r)) = r ∩ t

Tactic:
simp [Set.ext_iff]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinitesimal_pos_iff_infinitePos_inv {x : ℝ*} :
    InfinitePos x⁻¹ ↔ Infinitesimal x ∧ 0 < x :=
  infinitePos_iff_infinitesimal_inv_pos.trans <| by rw [inv_inv]

Proof state:
x : ℝ*
⊢ x⁻¹⁻¹.Infinitesimal ∧ 0 < x⁻¹⁻¹ ↔ x.Infinitesimal ∧ 0 < x

Tactic:
rw [inv_inv]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem neg_congr {R} [Ring R] {a a' b : R} (_ : a = a')
    (_ : -a' = b) : (-a : R) = b

Proof state:
R : Type u_2
inst✝ : Ring R
a a' b : R
x✝¹ : a = a'
x✝ : -a' = b
⊢ -a = b

Tactic:
subst_vars

Result:
R : Type u_2
inst✝ : Ring R
a' : R
⊢ -a' = -a'

Proof state:
R : Type u_2
inst✝ : Ring R
a' : R
⊢ -a' = -a'

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem norm_mk_eq_zero (S : AddSubgroup M) (hS : IsClosed (S : Set M)) (m : M)
    (h : ‖mk' S m‖ = 0) : m ∈ S

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
hS : IsClosed ↑S
m : M
h : ‖(mk' S) m‖ = 0
⊢ m ∈ S

Tactic:
rwa [quotient_norm_eq_zero_iff, hS.closure_eq] at h

Result:
no goals
-- Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean
theorem le_maximalIdeal {J : Ideal R} (hJ : J ≠ ⊤) : J ≤ maximalIdeal R

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
J : Ideal R
hJ : J ≠ ⊤
M : Ideal R
hM1 : M.IsMaximal
hM2 : J ≤ M
⊢ J ≤ maximalIdeal R

Tactic:
rwa [← eq_maximalIdeal hM1]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
J : Ideal R
hJ : J ≠ ⊤
⊢ J ≤ maximalIdeal R

Tactic:
rcases Ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
J : Ideal R
hJ : J ≠ ⊤
M : Ideal R
hM1 : M.IsMaximal
hM2 : J ≤ M
⊢ J ≤ maximalIdeal R
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem unique_int_coeff_of_cycl {K : Type*} [CommRing K] [IsDomain K] [CharZero K] {ζ : K}
    {n : ℕ+} (h : IsPrimitiveRoot ζ n) :
    ∃! P : ℤ[X], map (Int.castRingHom K) P = cyclotomic' n K

Proof state:
case intro
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ P.degree = (cyclotomic' (↑n) K).degree ∧ P.Monic
⊢ ∃! P, map (Int.castRingHom K) P = cyclotomic' (↑n) K

Tactic:
refine ⟨P, hP.1, fun Q hQ => ?_⟩

Result:
case intro
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ P.degree = (cyclotomic' (↑n) K).degree ∧ P.Monic
Q : ℤ[X]
hQ : (fun P => map (Int.castRingHom K) P = cyclotomic' (↑n) K) Q
⊢ Q = P

Proof state:
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
⊢ ∃! P, map (Int.castRingHom K) P = cyclotomic' (↑n) K

Tactic:
obtain ⟨P, hP⟩ := int_coeff_of_cyclotomic' h

Result:
case intro
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ P.degree = (cyclotomic' (↑n) K).degree ∧ P.Monic
⊢ ∃! P, map (Int.castRingHom K) P = cyclotomic' (↑n) K

Proof state:
case intro.a
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ P.degree = (cyclotomic' (↑n) K).degree ∧ P.Monic
Q : ℤ[X]
hQ : (fun P => map (Int.castRingHom K) P = cyclotomic' (↑n) K) Q
⊢ map (Int.castRingHom K) Q = map (Int.castRingHom K) P

Tactic:
rw [hP.1, hQ]

Result:
no goals

Proof state:
case intro
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ P.degree = (cyclotomic' (↑n) K).degree ∧ P.Monic
Q : ℤ[X]
hQ : (fun P => map (Int.castRingHom K) P = cyclotomic' (↑n) K) Q
⊢ Q = P

Tactic:
apply map_injective (Int.castRingHom K) Int.cast_injective

Result:
case intro.a
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ P.degree = (cyclotomic' (↑n) K).degree ∧ P.Monic
Q : ℤ[X]
hQ : (fun P => map (Int.castRingHom K) P = cyclotomic' (↑n) K) Q
⊢ map (Int.castRingHom K) Q = map (Int.castRingHom K) P
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma Even.eval_neg (x : ZMod m) (hψ : ψ.Even) : ψ (- x) = ψ x

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = 1
⊢ ψ (-1) * ψ x = ψ x

Tactic:
simp [hψ]

Result:
no goals

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ.Even
⊢ ψ (-x) = ψ x

Tactic:
rw [Even] at hψ

Result:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = 1
⊢ ψ (-x) = ψ x

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = 1
⊢ ψ (-x) = ψ x

Tactic:
rw [← neg_one_mul, map_mul]

Result:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = 1
⊢ ψ (-1) * ψ x = ψ x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem size_eq_one {xs : Vector α 1} : ∃ a, xs = #v[a]

Proof state:
case mk
α : Type u_1
xs : Array α
h : xs.size = 1
⊢ ∃ a, { toArray := xs, size_toArray := h } = { toArray := #[a], size_toArray := ⋯ }

Tactic:
simpa using Array.size_eq_one.mp h

Result:
no goals

Proof state:
α : Type u_1
xs : Vector α 1
⊢ ∃ a, xs = { toArray := #[a], size_toArray := ⋯ }

Tactic:
rcases xs with ⟨xs, h⟩

Result:
case mk
α : Type u_1
xs : Array α
h : xs.size = 1
⊢ ∃ a, { toArray := xs, size_toArray := h } = { toArray := #[a], size_toArray := ⋯ }
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem _root_.Ordinal.lift_preOmega (o : Ordinal.{u}) :
    Ordinal.lift.{v} (preOmega o) = preOmega (Ordinal.lift.{v} o)

Proof state:
o : Ordinal.{u}
⊢ Ordinal.lift.{v, u} (preOmega o) = preOmega (Ordinal.lift.{v, u} o)

Tactic:
rw [← ord_preAleph, lift_ord, lift_preAleph, ord_preAleph]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem count_attach [DecidableEq α] (l : Array α) (a : {x // x ∈ l}) :
    l.attach.count a = l.count ↑a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : Array α
a : { x // x ∈ l }
⊢ count a l.attach = count a.val l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : { x // x ∈ { toList := l } }
⊢ count a { toList := l }.attach = count a.val { toList := l }

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : { x // x ∈ { toList := l } }
⊢ List.countP (fun x => x.val == a.val) (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯) = List.count a.val l

Tactic:
rw [List.countP_pmap, List.countP_attach (p := (fun x => x == a.1)), List.count]

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : { x // x ∈ { toList := l } }
⊢ count a { toList := l }.attach = count a.val { toList := l }

Tactic:
simp only [List.attach_toArray, List.attachWith_mem_toArray, List.count_toArray]

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : { x // x ∈ { toList := l } }
⊢ List.count a (List.map (fun x => ⟨x.val, ⋯⟩) l.attach) = List.count a.val l

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : { x // x ∈ { toList := l } }
⊢ List.countP (fun x => x == a) (List.pmap (fun a h => ⟨⟨a, h⟩.val, ⋯⟩) l ⋯) = List.count a.val l

Tactic:
simp only [Subtype.beq_iff]

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : { x // x ∈ { toList := l } }
⊢ List.countP (fun x => x.val == a.val) (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯) = List.count a.val l

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : { x // x ∈ { toList := l } }
⊢ List.count a (List.map (fun x => ⟨x.val, ⋯⟩) l.attach) = List.count a.val l

Tactic:
rw [List.map_attach, List.count_eq_countP]

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : { x // x ∈ { toList := l } }
⊢ List.countP (fun x => x == a) (List.pmap (fun a h => ⟨⟨a, h⟩.val, ⋯⟩) l ⋯) = List.count a.val l
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
theorem lt_one_iff_num_lt_denom {q : ℚ} : q < 1 ↔ q.num < q.den

Proof state:
q : ℚ
⊢ q < 1 ↔ q.num < ↑q.den

Tactic:
simp [Rat.lt_def]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIoc_injective_left (a : α) : Injective (Ι a)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ Injective (Ι a)

Tactic:
simpa only [uIoc_comm] using uIoc_injective_right a

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma mem_spectrum_inr_of_not_isUnit {R A : Type*} [CommRing R]
    [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A]
    (a : A) (r : R) (hr : ¬ IsUnit r) : r ∈ spectrum R (a : Unitization R A) :=
  fun h ↦ hr <| by simpa [map_sub] using h.map (fstHom R A)

Proof state:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
hr : ¬IsUnit r
h : r ∈ resolventSet R ↑a
⊢ IsUnit r

Tactic:
simpa [map_sub] using h.map (fstHom R A)

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem one : mapFun f (1 : 𝕎 R) = 1

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
⊢ mapFun (⇑f) 1 = 1

Tactic:
map_fun_tac

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Ideal.lean
theorem exists_pow_le_of_le_radical_of_fg_radical {R : Type*} [CommSemiring R] {I J : Ideal R}
    (hIJ : I ≤ J.radical) (hJ : J.radical.FG) :
    ∃ k : ℕ, I ^ k ≤ J

Proof state:
case intro
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
hIJ : I ≤ J.radical
hJ : J.radical.FG
k : ℕ
hk : J.radical ^ k ≤ J
⊢ ∃ k, I ^ k ≤ J

Tactic:
use k

Result:
case h
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
hIJ : I ≤ J.radical
hJ : J.radical.FG
k : ℕ
hk : J.radical ^ k ≤ J
⊢ I ^ k ≤ J

Proof state:
case h
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
hIJ : I ≤ J.radical
hJ : J.radical.FG
k : ℕ
hk : J.radical ^ k ≤ J
⊢ I ^ k ≤ J

Tactic:
calc
  I ^ k ≤ J.radical ^ k := Ideal.pow_right_mono hIJ _
  _ ≤ J := hk

Result:
no goals

Proof state:
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
hIJ : I ≤ J.radical
hJ : J.radical.FG
⊢ ∃ k, I ^ k ≤ J

Tactic:
obtain ⟨k, hk⟩ := J.exists_radical_pow_le_of_fg hJ

Result:
case intro
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
hIJ : I ≤ J.radical
hJ : J.radical.FG
k : ℕ
hk : J.radical ^ k ≤ J
⊢ ∃ k, I ^ k ≤ J
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sqrtTwoAddSeries_lt_two : ∀ n : ℕ, sqrtTwoAddSeries 0 n < 2
  | 0 => by norm_num
  | n + 1 => by
    refine lt_of_lt_of_le ?_ (sqrt_sq zero_lt_two.le).le
    rw [sqrtTwoAddSeries, sqrt_lt_sqrt_iff, ← lt_sub_iff_add_lt']
    · refine (sqrtTwoAddSeries_lt_two n).trans_le ?_
      norm_num
    · exact add_nonneg zero_le_two (sqrtTwoAddSeries_zero_nonneg n)

Proof state:
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
exact add_nonneg zero_le_two (sqrtTwoAddSeries_zero_nonneg n)

Result:
no goals

Proof state:
⊢ sqrtTwoAddSeries 0 0 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
⊢ 2 ≤ 2 ^ 2 - 2

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2 ^ 2 - 2

Tactic:
refine (sqrtTwoAddSeries_lt_two n).trans_le ?_

Result:
n : ℕ
⊢ 2 ≤ 2 ^ 2 - 2

Proof state:
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < 2

Tactic:
refine lt_of_lt_of_le ?_ (sqrt_sq zero_lt_two.le).le

Result:
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < √(2 ^ 2)

Proof state:
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < √(2 ^ 2)

Tactic:
rw [sqrtTwoAddSeries, sqrt_lt_sqrt_iff, ← lt_sub_iff_add_lt']

Result:
n : ℕ
⊢ sqrtTwoAddSeries 0 n < 2 ^ 2 - 2

n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
/-- A diagonal matrix is hermitian if each diagonal entry is self-adjoint -/
lemma isHermitian_diagonal_iff [DecidableEq n] {d : n → α} :
    IsHermitian (diagonal d) ↔ (∀ i : n, IsSelfAdjoint (d i))

Proof state:
α : Type u_1
n : Type u_4
inst✝² : AddMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : DecidableEq n
d : n → α
⊢ (diagonal d).IsHermitian ↔ ∀ (i : n), IsSelfAdjoint (d i)

Tactic:
simp [isSelfAdjoint_iff, IsHermitian, conjTranspose, diagonal_transpose, diagonal_map]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Basic.lean
lemma mk_sub {x y : PGame} (hx : x.Numeric) (hy : y.Numeric) :
    Surreal.mk (x - y) (hx.sub hy) = Surreal.mk x hx - Surreal.mk y hy

Proof state:
x y : PGame
hx : x.Numeric
hy : y.Numeric
⊢ mk (x - y) ⋯ = mk x hx - mk y hy

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/NoncommCoprod.lean
theorem noncommCoprod_apply' (comm) (mn : M × N) :
    (f.noncommCoprod g comm) mn = g mn.2 * f mn.1

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
mn : M × N
⊢ (f.noncommCoprod g comm) mn = g mn.2 * f mn.1

Tactic:
rw [← comm, MonoidHom.noncommCoprod_apply]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem ofInt'_neg : ∀ n : ℤ, ofInt' (-n) = -ofInt' n
  | -[n+1] => show ofInt' (n + 1 : ℕ) = _ by simp only [ofInt', Num.zneg_toZNumNeg]
  | 0 => show Num.toZNum (Num.ofNat' 0) = -Num.toZNum (Num.ofNat' 0) by rw [Num.ofNat'_zero]; rfl
  | (n + 1 : ℕ) => show Num.toZNumNeg _ = -Num.toZNum _ by rw [Num.zneg_toZNum]

Proof state:
⊢ Num.toZNum 0 = -Num.toZNum 0

Tactic:
rfl

Result:
no goals

Proof state:
⊢ (Num.ofNat' 0).toZNum = -(Num.ofNat' 0).toZNum

Tactic:
rw [Num.ofNat'_zero]

Result:
⊢ Num.toZNum 0 = -Num.toZNum 0

Proof state:
n : ℕ
⊢ ofInt' ↑(n + 1) = -ofInt' -[n+1]

Tactic:
simp only [ofInt', Num.zneg_toZNumNeg]

Result:
no goals

Proof state:
n : ℕ
⊢ (Num.ofNat' (n + 1)).toZNumNeg = -(Num.ofNat' (n + 1)).toZNum

Tactic:
rw [Num.zneg_toZNum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n

Proof state:
m n : Nat
⊢ range m <+ range n ↔ m ≤ n

Tactic:
simp only [range_eq_range', range'_sublist_right]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity (hI : I ≠ ⊥) (hJ : J ≠ ⊥)
    (L : Ideal R) (hL : L ∈ normalizedFactors I) :
    emultiplicity (↑(normalizedFactorsEquivOfQuotEquiv f hI hJ ⟨L, hL⟩)) J = emultiplicity L I

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ ∀ (l l' : { l // l ∣ I }),
    ↑((idealFactorsEquivOfQuotEquiv f).toEquiv l) ∣ ↑((idealFactorsEquivOfQuotEquiv f).toEquiv l') ↔ ↑l ∣ ↑l'

Tactic:
exact fun ⟨l, hl⟩ ⟨l', hl'⟩ => idealFactorsEquivOfQuotEquiv_is_dvd_iso f hl hl'

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ emultiplicity (↑((idealFactorsEquivOfQuotEquiv f) ⟨↑⟨L, hL⟩, ⋯⟩)) J = emultiplicity L I

Tactic:
refine emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors hI hJ hL
  (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ ∀ (l l' : { l // l ∣ I }),
    ↑((idealFactorsEquivOfQuotEquiv f).toEquiv l) ∣ ↑((idealFactorsEquivOfQuotEquiv f).toEquiv l') ↔ ↑l ∣ ↑l'

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ emultiplicity (↑((normalizedFactorsEquivOfQuotEquiv f hI hJ) ⟨L, hL⟩)) J = emultiplicity L I

Tactic:
rw [normalizedFactorsEquivOfQuotEquiv, Equiv.coe_fn_mk, Subtype.coe_mk]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ emultiplicity (↑((idealFactorsEquivOfQuotEquiv f) ⟨↑⟨L, hL⟩, ⋯⟩)) J = emultiplicity L I
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem eq_of_forall_symmetric {α : Type*} [UniformSpace α] [T0Space α] {x y : α}
    (h : ∀ {V}, V ∈ 𝓤 α → SymmetricRel V → (x, y) ∈ V) : x = y :=
  eq_of_uniformity_basis hasBasis_symmetric (by simpa)

Proof state:
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
x y : α
h : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → (x, y) ∈ V
⊢ ∀ {i : Set (α × α)}, i ∈ 𝓤 α ∧ SymmetricRel i → (x, y) ∈ id i

Tactic:
simpa

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem lift_includeLeft_includeRight :
    lift includeLeft includeRight (fun _ _ => (Commute.one_right _).tmul (Commute.one_left _)) =
      .id S (A ⊗[R] B)

Proof state:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ lift includeLeft includeRight ⋯ = AlgHom.id S (A ⊗[R] B)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_eq_prod_diff_singleton_mul [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s)
    (f : α → β) : ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∈ s
f : α → β
⊢ ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i

Tactic:
rw [prod_eq_mul_prod_diff_singleton h, mul_comm]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem toIntermediateField'_toSubalgebra (S : IntermediateField K L) :
    S.toSubalgebra.toIntermediateField' (Field.toIsField S) = S

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
⊢ S.toIntermediateField' ⋯ = S

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x✝ : L
⊢ x✝ ∈ S.toIntermediateField' ⋯ ↔ x✝ ∈ S

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x✝ : L
⊢ x✝ ∈ S.toIntermediateField' ⋯ ↔ x✝ ∈ S

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
theorem bit_add : ∀ (b : Bool) (n m : ℕ), bit b (n + m) = bit false n + bit b m
  | true,  _, _ => by dsimp [bit]; omega
  | false, _, _ => by dsimp [bit]; omega

Proof state:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) = 2 * x✝¹ + 2 * x✝

Tactic:
omega

Result:
no goals

Proof state:
x✝¹ x✝ : ℕ
⊢ bit false (x✝¹ + x✝) = bit false x✝¹ + bit false x✝

Tactic:
dsimp [bit]

Result:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) = 2 * x✝¹ + 2 * x✝

Proof state:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + (2 * x✝ + 1)

Tactic:
omega

Result:
no goals

Proof state:
x✝¹ x✝ : ℕ
⊢ bit true (x✝¹ + x✝) = bit false x✝¹ + bit true x✝

Tactic:
dsimp [bit]

Result:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + (2 * x✝ + 1)
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem binomial_spec [DecidableEq α] (hab : a ≠ b) :
    (f a)! * (f b)! * multinomial {a, b} f = (f a + f b)!

Proof state:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
⊢ (f a)! * (f b)! * multinomial {a, b} f = (f a + f b)!

Tactic:
simpa [Finset.sum_pair hab, Finset.prod_pair hab] using multinomial_spec {a, b} f

Result:
no goals
-- Mathlib/Topology/UniformSpace/Dini.lean
/-- **Dini's theorem**: if `F n` is a monotone increasing collection of continuous functions on a
set `s` converging pointwise to a continuous function `f`, then `F n` converges locally uniformly
to `f`. -/
lemma tendstoLocallyUniformlyOn_of_forall_tendsto {s : Set α}
    (hF_cont : ∀ i, ContinuousOn (F i) s) (hF_mono : ∀ x ∈ s, Monotone (F · x))
    (hf : ContinuousOn f s) (h_tendsto : ∀ x ∈ s, Tendsto (F · x) atTop (𝓝 (f x))) :
    TendstoLocallyUniformlyOn F f atTop s

Proof state:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
s : Set α
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_mono : ∀ x ∈ s, Monotone fun x_1 => F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformlyOn F f atTop s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe]

Result:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
s : Set α
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_mono : ∀ x ∈ s, Monotone fun x_1 => F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) atTop
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem bind₁_comp_bind₁ {υ : Type*} (f : σ → MvPolynomial τ R) (g : τ → MvPolynomial υ R) :
    (bind₁ g).comp (bind₁ f) = bind₁ fun i => bind₁ g (f i)

Proof state:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
i✝ : σ
⊢ ((bind₁ g).comp (bind₁ f)) (X i✝) = (bind₁ fun i => (bind₁ g) (f i)) (X i✝)

Tactic:
apply bind₁_bind₁

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
⊢ (bind₁ g).comp (bind₁ f) = bind₁ fun i => (bind₁ g) (f i)

Tactic:
ext1

Result:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
i✝ : σ
⊢ ((bind₁ g).comp (bind₁ f)) (X i✝) = (bind₁ fun i => (bind₁ g) (f i)) (X i✝)
-- Mathlib/Data/Set/Lattice.lean
theorem preimage_iUnion {f : α → β} {s : ι → Set β} : (f ⁻¹' ⋃ i, s i) = ⋃ i, f ⁻¹' s i :=
  Set.ext <| by simp [preimage]

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
⊢ ∀ (x : α), x ∈ f ⁻¹' ⋃ i, s i ↔ x ∈ ⋃ i, f ⁻¹' s i

Tactic:
simp [preimage]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem _root_.GroupWithZero.eq_zero_or_unit (a : G₀) : a = 0 ∨ ∃ u : G₀ˣ, a = u

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a = 0 ∨ ∃ u, a = ↑u

Tactic:
simpa using em _

Result:
no goals