harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
theorem totient_le_degree_minpoly : Nat.totient n ≤ (minpoly ℤ μ).natDegree

Proof state:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
P : ℤ[X] := minpoly ℤ μ
⊢ n.totient ≤ (minpoly ℤ μ).natDegree

Tactic:
let P_K : K[X] := map (Int.castRingHom K) P

Result:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ n.totient ≤ (minpoly ℤ μ).natDegree

Proof state:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
⊢ n.totient ≤ (minpoly ℤ μ).natDegree

Tactic:
let P : ℤ[X] := minpoly ℤ μ

Result:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
P : ℤ[X] := minpoly ℤ μ
⊢ n.totient ≤ (minpoly ℤ μ).natDegree

Proof state:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ n.totient ≤ (minpoly ℤ μ).natDegree

Tactic:
calc
  n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
  _ ≤ P_K.roots.toFinset.card := Finset.card_le_card (is_roots_of_minpoly h)
  _ ≤ Multiset.card P_K.roots := Multiset.toFinset_card_le _
  _ ≤ P_K.natDegree := card_roots' _
  _ ≤ P.natDegree := natDegree_map_le

Result:
no goals

Proof state:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
⊢ n.totient ≤ (minpoly ℤ μ).natDegree

Tactic:
classical
let P : ℤ[X] := minpoly ℤ μ
let P_K : K[X] := map (Int.castRingHom K) P
calc
  n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
  _ ≤ P_K.roots.toFinset.card := Finset.card_le_card (is_roots_of_minpoly h)
  _ ≤ Multiset.card P_K.roots := Multiset.toFinset_card_le _
  _ ≤ P_K.natDegree := card_roots' _
  _ ≤ P.natDegree := natDegree_map_le

Result:
no goals
-- Mathlib/Data/Tree/Traversable.lean
lemma naturality {F G : Type u → Type*} [Applicative F] [Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {β : Type u} (f : α → F β)
    (t : Tree α) : η (t.traverse f) = t.traverse (η.app β ∘ f : α → G β)

Proof state:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
t : Tree α
⊢ (fun {α} => η.app α) (traverse f t) = traverse (η.app β ∘ f) t

Tactic:
induction t with
| nil => rw [traverse, traverse, η.preserves_pure]
| node v l r hl hr =>
  rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
    Function.comp_apply]

Result:
no goals

Proof state:
case nil
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
⊢ (fun {α} => η.app α) (traverse f nil) = traverse (η.app β ∘ f) nil

Tactic:
rw [traverse, traverse, η.preserves_pure]

Result:
no goals

Proof state:
case node
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : Tree α
hl : (fun {α} => η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α} => η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ (fun {α} => η.app α) (traverse f (node v l r)) = traverse (η.app β ∘ f) (node v l r)

Tactic:
rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
  Function.comp_apply]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
lemma chainTopCoeff_zero_right [Nontrivial L] (hα : α.IsNonZero) :
    chainTopCoeff α (0 : Weight K H L) = 1

Proof state:
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
⊢ ∃ k, k • f = ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1)) x

Tactic:
have : (toEnd K L L f ^ (chainTopCoeff α (0 : Weight K H L) + 1)) x ∈ rootSpace H (-α) := by
  convert toEnd_pow_apply_mem hf hx (chainTopCoeff α (0 : Weight K H L) + 1) using 2
  rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
    add_assoc, smul_neg, neg_add_cancel, add_zero]

Result:
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
this : ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1)) x ∈ rootSpace H (-⇑α)
⊢ ∃ k, k • f = ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1)) x

Proof state:
case hab
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
⊢ chainTopCoeff (⇑α) 0 ≠ 0

Tactic:
intro e

Result:
case hab
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
e : chainTopCoeff (⇑α) 0 = 0
⊢ False
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem cokernelIsoOfEq_trans {f g h : X ⟶ Y} [HasCokernel f] [HasCokernel g] [HasCokernel h]
    (w₁ : f = g) (w₂ : g = h) :
    cokernelIsoOfEq w₁ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq (w₁.trans w₂)

Proof state:
case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f h : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel h
inst✝ : HasCokernel f
w₂ : f = h
⊢ cokernelIsoOfEq ⋯ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq ⋯

Tactic:
cases w₂

Result:
case refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasCokernel f
⊢ cokernelIsoOfEq ⋯ ≪≫ cokernelIsoOfEq ⋯ = cokernelIsoOfEq ⋯

Proof state:
case refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasCokernel f
⊢ cokernelIsoOfEq ⋯ ≪≫ cokernelIsoOfEq ⋯ = cokernelIsoOfEq ⋯

Tactic:
ext

Result:
case refl.refl.w.h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasCokernel f
⊢ coequalizer.π f 0 ≫ (cokernelIsoOfEq ⋯ ≪≫ cokernelIsoOfEq ⋯).hom = coequalizer.π f 0 ≫ (cokernelIsoOfEq ⋯).hom

Proof state:
case refl.refl.w.h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasCokernel f
⊢ coequalizer.π f 0 ≫ (cokernelIsoOfEq ⋯ ≪≫ cokernelIsoOfEq ⋯).hom = coequalizer.π f 0 ≫ (cokernelIsoOfEq ⋯).hom

Tactic:
simp [cokernelIsoOfEq]

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f g h : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel g
inst✝ : HasCokernel h
w₁ : f = g
w₂ : g = h
⊢ cokernelIsoOfEq w₁ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq ⋯

Tactic:
cases w₁

Result:
case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f h : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel h
inst✝ : HasCokernel f
w₂ : f = h
⊢ cokernelIsoOfEq ⋯ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq ⋯
-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem abs_sub_convs_le (not_terminatedAt_n : ¬(of v).TerminatedAt n) :
    |v - (of v).convs n| ≤ 1 / ((of v).dens n * ((of v).dens <| n + 1))

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
⊢ nextConts.b = pred_conts.b + gp.b * conts.b

Tactic:
simp [nextConts, contsAux_recurrence s_nth_eq pred_conts_eq conts_eq, gp_a_eq_one,
  pred_conts_eq.symm, conts_eq.symm, add_comm]

Result:
no goals

Proof state:
case intro.intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
⊢ |v - g.convs n| ≤ 1 / den

Tactic:
obtain ⟨ifp_n, stream_nth_eq, stream_nth_fr_ne_zero, if_of_eq_ifp_succ_n⟩ :
  ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0
    ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
  IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq

Result:
case intro.intro.intro.intro.intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
⊢ |v - g.convs n| ≤ 1 / den
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem mul_X_sub_intCast_comp {n : ℕ} :
    (p * (X - (n : R[X]))).comp q = p.comp q * (q - n)

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
n : ℕ
⊢ (p * (X - ↑n)).comp q = p.comp q * (q - ↑n)

Tactic:
rw [mul_sub, sub_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_sub]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Basic.lean
lemma FermatLastTheoremWith'.fermatLastTheoremWith {α : Type*} [CommSemiring α] [IsDomain α]
    {n : ℕ} (h : FermatLastTheoremWith' α n)
    (hn : ∀ a b c : α, IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n) :
    FermatLastTheoremWith α n

Proof state:
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
n : ℕ
h : FermatLastTheoremWith' α n
hn : ∀ (a b c : α), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
⊢ FermatLastTheoremWith α n

Tactic:
intro a b c ha hb hc heq

Result:
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
n : ℕ
h : FermatLastTheoremWith' α n
hn : ∀ (a b c : α), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
a b c : α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
heq : a ^ n + b ^ n = c ^ n
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
n : ℕ
h : FermatLastTheoremWith' α n
hn : ∀ (a b c : α), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : α
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' * d) ^ n + (b' * d) ^ n = (c' * d) ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
⊢ False

Tactic:
rw [mul_pow, mul_pow, mul_pow, ← add_mul] at heq

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
n : ℕ
h : FermatLastTheoremWith' α n
hn : ∀ (a b c : α), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : α
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
⊢ False

Proof state:
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
n : ℕ
h : FermatLastTheoremWith' α n
hn : ∀ (a b c : α), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
a b c : α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
heq : a ^ n + b ^ n = c ^ n
⊢ False

Tactic:
rcases h a b c ha hb hc heq with ⟨d, a', b', c', ⟨rfl, rfl, rfl⟩, ⟨ua, ub, uc⟩⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
n : ℕ
h : FermatLastTheoremWith' α n
hn : ∀ (a b c : α), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : α
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' * d) ^ n + (b' * d) ^ n = (c' * d) ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
n : ℕ
h : FermatLastTheoremWith' α n
hn : ∀ (a b c : α), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : α
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
⊢ False

Tactic:
exact hn _ _ _ ua ub uc <| mul_right_cancel₀ (pow_ne_zero _ (right_ne_zero_of_mul ha)) heq

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
theorem eq_of_slope_eq_zero {f : k → PE} {a b : k} (h : slope f a b = (0 : E)) : f a = f b

Proof state:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
h : slope f a b = 0
⊢ f a = f b

Tactic:
rw [← sub_smul_slope_vadd f a b, h, smul_zero, zero_vadd]

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem Finsupp.toFreeAbelianGroup_comp_singleAddHom (x : X) :
    Finsupp.toFreeAbelianGroup.comp (Finsupp.singleAddHom x) =
      (smulAddHom ℤ (FreeAbelianGroup X)).flip (of x)

Proof state:
X : Type u_1
x : X
⊢ toFreeAbelianGroup.comp (singleAddHom x) = (smulAddHom ℤ (FreeAbelianGroup X)).flip (of x)

Tactic:
ext

Result:
case h1
X : Type u_1
x : X
⊢ (toFreeAbelianGroup.comp (singleAddHom x)) 1 = ((smulAddHom ℤ (FreeAbelianGroup X)).flip (of x)) 1

Proof state:
case h1
X : Type u_1
x : X
⊢ (toFreeAbelianGroup.comp (singleAddHom x)) 1 = ((smulAddHom ℤ (FreeAbelianGroup X)).flip (of x)) 1

Tactic:
simp only [AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply, one_smul,
  toFreeAbelianGroup, Finsupp.liftAddHom_apply_single]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_empty {a : α} {c} : (empty c : Raw₀ α β).getKey? a = none

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
c : Nat
⊢ (empty c).getKey? a = none

Tactic:
simp [getKey?]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem y_eq_one_of_mem_closedBall {D : ℝ} {x : E} (Dpos : 0 < D)
    (hx : x ∈ closedBall (0 : E) (1 - D)) : y D x = 1

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
⊢ ball x D ⊆ ball 0 1

Tactic:
apply ball_subset_ball'

Result:
case h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
⊢ D + dist x 0 ≤ 1

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
C : ball x D ⊆ ball 0 1
⊢ ∀ y ∈ ball x D, φ y = 1

Tactic:
intro y hy

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
C : ball x D ⊆ ball 0 1
y : E
hy : y ∈ ball x D
⊢ φ y = 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem limplies_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
    Limplies (PosFin n) (insert f c) f

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ p ⊨ f.insert c → p ⊨ f

Tactic:
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ (∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x) → ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'

Tactic:
have c'_in_fc : c' ∈ toList (insert f c) := by
  simp only [insert_iff, Array.toList_toArray, List.mem_singleton]
  exact Or.inr c'_in_f

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'

Tactic:
exact h c' c'_in_fc

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ (∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x) → ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x

Tactic:
intro h c' c'_in_f

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ c' ∈ (f.insert c).toList

Tactic:
simp only [insert_iff, Array.toList_toArray, List.mem_singleton]

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ c' = c ∨ c' ∈ f.toList

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ c' = c ∨ c' ∈ f.toList

Tactic:
exact Or.inr c'_in_f

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ Limplies (PosFin n) (f.insert c) f

Tactic:
intro p

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ p ⊨ f.insert c → p ⊨ f
-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
theorem baseChange_ext ⦃Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁⦄
    (h : ∀ m, Q₁ (1 ⊗ₜ m) = Q₂ (1 ⊗ₜ m)) :
    Q₁ = Q₂

Proof state:
case H.add
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
⊢ Q₁ (x + y) = Q₂ (x + y)

Tactic:
have : Q₁.polarBilin = Q₂.polarBilin := by
  ext
  dsimp [polar]
  rw [← TensorProduct.tmul_add, h, h, h]

Result:
case H.add
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x y : A ⊗[R] M₂
hx : Q₁ x = Q₂ x
hy : Q₁ y = Q₂ y
this : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁ (x + y) = Q₂ (x + y)

Proof state:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)
a : A
m : M₂
⊢ Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)

Tactic:
rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h]

Result:
no goals

Proof state:
case H.tmul
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x✝ : A
y✝ : M₂
⊢ Q₁ (x✝ ⊗ₜ[R] y✝) = Q₂ (x✝ ⊗ₜ[R] y✝)

Tactic:
simp [h]

Result:
no goals

Proof state:
case H
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x : A ⊗[R] M₂
⊢ Q₁ x = Q₂ x

Tactic:
induction x with
| tmul => simp [h]
| zero => simp
| add x y hx hy =>
  have : Q₁.polarBilin = Q₂.polarBilin := by
    ext
    dsimp [polar]
    rw [← TensorProduct.tmul_add, h, h, h]
  replace := congr($this x y)
  dsimp [polar] at this
  linear_combination (norm := module) this + hx + hy

Result:
no goals
-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
/-- The **valuative criterion** for separated morphisms. -/
@[stacks 01L0]
lemma IsSeparated.of_valuativeCriterion [QuasiSeparated f]
    (hf : ValuativeCriterion.Uniqueness f) : IsSeparated f where
  diagonal_isClosedImmersion

Proof state:
case hf
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (pullback.diagonal f)
this : QuasiCompact (pullback.diagonal f)
⊢ IsClosed (Set.range ⇑(ConcreteCategory.hom (pullback.diagonal f).base))

Tactic:
apply IsClosedMap.isClosed_range

Result:
case hf.hf
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (pullback.diagonal f)
this : QuasiCompact (pullback.diagonal f)
⊢ IsClosedMap ⇑(ConcreteCategory.hom (pullback.diagonal f).base)