harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem calc_deriv_dist {z z' z1 : ℤ_[p]} (hz' : z' = z - z1)
    (hz1 : ‖z1‖ = ‖F.eval z‖ / ‖F.derivative.eval a‖) {n} (hz : ih n z) :
    ‖F.derivative.eval z' - F.derivative.eval z‖ < ‖F.derivative.eval a‖ :=
  calc
    ‖F.derivative.eval z' - F.derivative.eval z‖ ≤ ‖z' - z‖ := padic_polynomial_dist _ _ _
    _ = ‖z1‖

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖z' - z‖ = ‖z1‖

Tactic:
simp only [sub_eq_add_neg, add_assoc, hz', add_add_neg_cancel'_right, norm_neg]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ≤
    ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
gcongr

Result:
case hab
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n

Proof state:
case hab
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n

Tactic:
apply hz.2

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem prod_top : (prod ⊤ ⊤ : NonUnitalSubalgebra R (A × B)) = ⊤

Proof state:
case h
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
⊢ ⊤.prod ⊤ = ⊤

Tactic:
ext

Result:
case h
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤
-- Mathlib/Data/Set/Prod.lean
theorem mk_preimage_prod_right_eq_if [DecidablePred (· ∈ s)] :
    Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
inst✝ : DecidablePred fun x => x ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_insert_le (a : α) (s : Finset α) : #(insert a s) ≤ #s + 1

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ #s ≤ #s + 1

Tactic:
exact Nat.le_succ _

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ #(insert a s) ≤ #s + 1

Tactic:
rw [card_insert_of_not_mem h]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ #(insert a s) ≤ #s + 1

Tactic:
rw [insert_eq_of_mem h]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ #s ≤ #s + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ #(insert a s) ≤ #s + 1

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ #(insert a s) ≤ #s + 1

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ #(insert a s) ≤ #s + 1
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma pullback_eq_of_not_isInvertible {f : E → F} {x : E}
    (h : ¬(fderiv 𝕜 f x).IsInvertible) (V : F → F) :
    pullback 𝕜 f V x = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ¬(fderiv 𝕜 f x).IsInvertible
V : F → F
⊢ pullback 𝕜 f V x = 0

Tactic:
simp [pullback, h]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma pullback_functorPushforward_equivalence_eq {X : C} (S : Sieve X) :
    Sieve.pullback (e.unit.app X) (Sieve.functorPushforward e.inverse
      (Sieve.functorPushforward e.functor S)) = S

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ (𝟭 C).obj X
⊢ (pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S))).arrows f✝ ↔ S.arrows f✝

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
S : Sieve X
⊢ pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S)) = S

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ (𝟭 C).obj X
⊢ (pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S))).arrows f✝ ↔ S.arrows f✝
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem restrict_coeSubgraph {G' : G.Subgraph} (G'' : G'.coe.Subgraph) :
    Subgraph.restrict (Subgraph.coeSubgraph G'') = G''

Proof state:
case verts.h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝ : ↑G'.verts
⊢ x✝ ∈ (Subgraph.restrict (Subgraph.coeSubgraph G'')).verts ↔ x✝ ∈ G''.verts

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
⊢ Subgraph.restrict (Subgraph.coeSubgraph G'') = G''

Tactic:
ext

Result:
case verts.h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝ : ↑G'.verts
⊢ x✝ ∈ (Subgraph.restrict (Subgraph.coeSubgraph G'')).verts ↔ x✝ ∈ G''.verts

case Adj.h.h.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ (Subgraph.restrict (Subgraph.coeSubgraph G'')).Adj x✝¹ x✝ ↔ G''.Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ (G'.Adj ↑x✝¹ ↑x✝ ∧ ∃ (hv : ↑x✝¹ ∈ G'.verts) (hw : ↑x✝ ∈ G'.verts), G''.Adj ⟨↑x✝¹, hv⟩ ⟨↑x✝, hw⟩) ↔ G''.Adj x✝¹ x✝

Tactic:
simpa using G''.adj_sub

Result:
no goals

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ (Subgraph.restrict (Subgraph.coeSubgraph G'')).Adj x✝¹ x✝ ↔ G''.Adj x✝¹ x✝

Tactic:
rw [restrict_adj, coeSubgraph_adj]

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ (G'.Adj ↑x✝¹ ↑x✝ ∧ ∃ (hv : ↑x✝¹ ∈ G'.verts) (hw : ↑x✝ ∈ G'.verts), G''.Adj ⟨↑x✝¹, hv⟩ ⟨↑x✝, hw⟩) ↔ G''.Adj x✝¹ x✝
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negDblY_eq {P : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) : W.negDblY P =
    (-eval P W.polynomialX * (eval P W.polynomialX ^ 2
      - W.a₁ * eval P W.polynomialX * P z * (P y - W.negY P)
      - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 - 2 * P x * P z * (P y - W.negY P) ^ 2
      - P x * P z * (P y - W.negY P) ^ 2) + P y * P z ^ 2 * (P y - W.negY P) ^ 3) / P z ^ 2

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
⊢ W.negDblY P =
    (-(eval P) W.polynomialX *
          ((eval P) W.polynomialX ^ 2 - W.a₁ * (eval P) W.polynomialX * P z * (P y - W.negY P) -
                W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
              2 * P x * P z * (P y - W.negY P) ^ 2 -
            P x * P z * (P y - W.negY P) ^ 2) +
        P y * P z ^ 2 * (P y - W.negY P) ^ 3) /
      P z ^ 2

Tactic:
rw [← negDblY_eq' hP, mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_list_sum_le (l : List S[X]) :
    natDegree l.sum ≤ (l.map natDegree).foldr max 0

Proof state:
case hadd
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ ∀ (x y : S[X]), (x + y).natDegree ≤ x.natDegree ⊔ y.natDegree

Tactic:
exact natDegree_add_le

Result:
no goals

Proof state:
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ l.sum.natDegree ≤ List.foldr max 0 (List.map natDegree l)

Tactic:
apply List.sum_le_foldr_max natDegree

Result:
case h0
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ natDegree 0 ≤ 0

case hadd
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ ∀ (x y : S[X]), (x + y).natDegree ≤ x.natDegree ⊔ y.natDegree

Proof state:
case h0
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ natDegree 0 ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_eq_lsub_or_sup_succ_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) :
    sup.{_, v} f = lsub.{_, v} f ∨ succ (sup.{_, v} f) = lsub.{_, v} f

Proof state:
case inl
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = lsub f
⊢ sup f = lsub f ∨ succ (sup f) = lsub f

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ sup f = lsub f ∨ succ (sup f) = lsub f

Tactic:
rcases eq_or_lt_of_le (sup_le_lsub.{_, v} f) with h | h

Result:
case inl
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = lsub f
⊢ sup f = lsub f ∨ succ (sup f) = lsub f

case inr
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f < lsub f
⊢ sup f = lsub f ∨ succ (sup f) = lsub f

Proof state:
case inr
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f < lsub f
⊢ sup f = lsub f ∨ succ (sup f) = lsub f

Tactic:
exact Or.inr ((succ_le_of_lt h).antisymm (lsub_le_sup_succ f))

Result:
no goals
-- Mathlib/Algebra/Order/Group/Defs.lean
theorem inv_le_self_iff : a⁻¹ ≤ a ↔ 1 ≤ a

Proof state:
α : Type u
inst✝ : LinearOrderedCommGroup α
a : α
⊢ a⁻¹ ≤ a ↔ 1 ≤ a

Tactic:
simp [inv_le_iff_one_le_mul']

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem sign_eq_ediv_abs (a : ℤ) : sign a = a / |a| :=
  if az : a = 0 then by simp [az]
  else (Int.ediv_eq_of_eq_mul_left (mt abs_eq_zero.1 az) (sign_mul_abs _).symm).symm

Proof state:
a : ℤ
az : a = 0
⊢ a.sign = a / |a|

Tactic:
simp [az]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_neg_self_of_nonzero {x : V} (hx : x ≠ 0) : angle (-x) x = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ angle (-x) x = π

Tactic:
rw [angle_comm, angle_self_neg_of_nonzero hx]

Result:
no goals
-- Mathlib/Topology/LocallyFinite.lean
theorem locallyFinite_option {f : Option ι → Set X} :
    LocallyFinite f ↔ LocallyFinite (f ∘ some)

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ↔ LocallyFinite (f ∘ some)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ some)

Tactic:
rw [← (Equiv.optionEquivSumPUnit.{0, _} ι).symm.locallyFinite_comp_iff, locallyFinite_sum]

Result:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) ↔
    LocallyFinite (f ∘ some)

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) ↔
    LocallyFinite (f ∘ some)

Tactic:
simp only [locallyFinite_of_finite, and_true]

Result:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ↔ LocallyFinite (f ∘ some)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem sub_emod_emod (m n k : Int) : (m - n % k) % k = (m - n) % k

Proof state:
m n k : Int
⊢ (m - n % k) % k = (m - n) % k

Tactic:
apply (emod_add_cancel_right (n % k)).mp

Result:
m n k : Int
⊢ (m - n % k + n % k) % k = (m - n + n % k) % k

Proof state:
m n k : Int
⊢ (m - n % k + n % k) % k = (m - n + n % k) % k

Tactic:
rw [Int.sub_add_cancel, Int.add_emod_emod, Int.sub_add_cancel]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean
theorem structuralIsoOfExpr_comp {f g h : a ⟶ b}
    (η : f ⟶ g) (η' : f ≅ g) (ih_η : η'.hom = η)
    (θ : g ⟶ h) (θ' : g ≅ h) (ih_θ : θ'.hom = θ) :
    (η' ≪≫ θ').hom  = η ≫ θ

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g h : a ⟶ b
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : g ⟶ h
θ' : g ≅ h
ih_θ : θ'.hom = θ
⊢ (η' ≪≫ θ').hom = η ≫ θ

Tactic:
simp [ih_η, ih_θ]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Flag.lean
theorem flag_covBy (b : Basis (Fin n) K V) (i : Fin n) :
    b.flag i.castSucc ⋖ b.flag i.succ

Proof state:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
⊢ b.flag i.castSucc ⋖ span K {b i} ⊔ b.flag i.castSucc

Tactic:
apply covBy_span_singleton_sup

Result:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
⊢ b i ∉ b.flag i.castSucc

Proof state:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
⊢ b.flag i.castSucc ⋖ b.flag i.succ

Tactic:
rw [flag_succ]

Result:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
⊢ b.flag i.castSucc ⋖ span K {b i} ⊔ b.flag i.castSucc

Proof state:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
⊢ b i ∉ b.flag i.castSucc

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] {a fallback : α} :
    ¬a ∈ m → m.getKeyD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
a fallback : α
⊢ ¬a ∈ m → m.getKeyD a fallback = fallback

Tactic:
simpa [mem_iff_contains] using getKeyD_eq_fallback_of_contains_eq_false

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem coeff_hsum_eq_sum {s : SummableFamily Γ R α} {g : Γ} :
    s.hsum.coeff g = ∑ i ∈ (s.coeff g).support, (s i).coeff g

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
⊢ s.hsum.coeff g = ∑ i ∈ (s.coeff g).support, (s i).coeff g

Tactic:
simp only [coeff_hsum, finsum_eq_sum _ (s.finite_co_support _), coeff_support]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma cfcₙ_real_eq_complex {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a

Proof state:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
f : ℝ → ℝ
ha : IsSelfAdjoint a
⊢ cfcₙ f a = cfcₙ (fun x => ↑(f x.re)) a

Tactic:
exact ha.quasispectrumRestricts.2.cfcₙ_eq_restrict (f := Complex.reCLM)
  Complex.isometry_ofReal.isUniformEmbedding ha ha.isStarNormal f

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
f : ℝ → ℝ
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ cfcₙ f a = cfcₙ (fun x => ↑(f x.re)) a

Tactic:
replace ha : IsSelfAdjoint a := ha

Result:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
f : ℝ → ℝ
ha : IsSelfAdjoint a
⊢ cfcₙ f a = cfcₙ (fun x => ↑(f x.re)) a
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem rightAdjointUniq_trans {F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
    (adj3 : F ⊣ G'') :
    (rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom =
      (rightAdjointUniq adj1 adj3).hom

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
⊢ (adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom = (adj1.rightAdjointUniq adj3).hom

Tactic:
simp [rightAdjointUniq]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_add_of_principal_mul_opow (hb : 1 < b) (ho : Principal (· * ·) (b ^ o)) :
    Principal (· + ·) o

Proof state:
b o : Ordinal.{u}
hb : 1 < b
ho : Principal (fun x1 x2 => x1 * x2) (b ^ o)
⊢ Principal (fun x1 x2 => x1 + x2) o

Tactic:
intro x y hx hy

Result:
b o : Ordinal.{u}
hb : 1 < b
ho : Principal (fun x1 x2 => x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
⊢ (fun x1 x2 => x1 + x2) x y < o

Proof state:
b o : Ordinal.{u}
hb : 1 < b
ho : Principal (fun x1 x2 => x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : (fun x1 x2 => x1 * x2) (b ^ x) (b ^ y) < b ^ o
⊢ (fun x1 x2 => x1 + x2) x y < o

Tactic:
dsimp only at *

Result:
b o : Ordinal.{u}
hb : 1 < b
ho : Principal (fun x1 x2 => x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : b ^ x * b ^ y < b ^ o
⊢ x + y < o

Proof state:
b o : Ordinal.{u}
hb : 1 < b
ho : Principal (fun x1 x2 => x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
⊢ (fun x1 x2 => x1 + x2) x y < o

Tactic:
have := ho ((opow_lt_opow_iff_right hb).2 hx) ((opow_lt_opow_iff_right hb).2 hy)

Result:
b o : Ordinal.{u}
hb : 1 < b
ho : Principal (fun x1 x2 => x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : (fun x1 x2 => x1 * x2) (b ^ x) (b ^ y) < b ^ o
⊢ (fun x1 x2 => x1 + x2) x y < o

Proof state:
b o : Ordinal.{u}
hb : 1 < b
ho : Principal (fun x1 x2 => x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : b ^ x * b ^ y < b ^ o
⊢ x + y < o

Tactic:
rwa [← opow_add, opow_lt_opow_iff_right hb] at this

Result:
no goals
-- Mathlib/Analysis/Complex/Angle.lean
lemma angle_div_left_eq_angle_mul_right (a x y : ℂ) : angle (x / a) y = angle x (y * a)

Proof state:
case inr
a x y : ℂ
ha : a ≠ 0
⊢ angle (x / a) y = angle x (y * a)

Tactic:
rw [← angle_mul_right ha, div_mul_cancel₀ _ ha]

Result:
no goals

Proof state:
case inl
x y : ℂ
⊢ angle (x / 0) y = angle x (y * 0)

Tactic:
simp

Result:
no goals

Proof state:
a x y : ℂ
⊢ angle (x / a) y = angle x (y * a)

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
x y : ℂ
⊢ angle (x / 0) y = angle x (y * 0)

case inr
a x y : ℂ
ha : a ≠ 0
⊢ angle (x / a) y = angle x (y * a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem min?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
    (replicate n a).min? = some a

Proof state:
α : Type u_1
inst✝ : Min α
n : Nat
a : α
w : min a a = a
h : 0 < n
⊢ (replicate n a).min? = some a

Tactic:
simp [min?_replicate, Nat.ne_of_gt h, w]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Canonical.lean
theorem tsub_mul [MulRightMono α] {a b c : α}
    (h : AddLECancellable (b * c)) : (a - b) * c = a * c - b * c

Proof state:
case inr
α : Type u
inst✝⁶ : NonUnitalNonAssocSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : CanonicallyOrderedAdd α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : MulRightMono α
a b c : α
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c

Tactic:
apply h.eq_tsub_of_add_eq

Result:
case inr
α : Type u
inst✝⁶ : NonUnitalNonAssocSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : CanonicallyOrderedAdd α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : MulRightMono α
a b c : α
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c + b * c = a * c

Proof state:
case inr
α : Type u
inst✝⁶ : NonUnitalNonAssocSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : CanonicallyOrderedAdd α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : MulRightMono α
a b c : α
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c + b * c = a * c

Tactic:
rw [← add_mul, tsub_add_cancel_of_le hba]

Result:
no goals

Proof state:
case inl
α : Type u
inst✝⁶ : NonUnitalNonAssocSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : CanonicallyOrderedAdd α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : MulRightMono α
a b c : α
h : AddLECancellable (b * c)
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

Tactic:
rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_right' hab c)]

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_setOf_le_re (a : ℝ) : frontier { z : ℂ | a ≤ z.re } = { z | z.re = a }

Proof state:
a : ℝ
⊢ frontier {z | a ≤ z.re} = {z | z.re = a}

Tactic:
simpa only [frontier_Ici] using frontier_preimage_re (Ici a)

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem filterMap_eq_flatMap_toList (f : α → Option β) (l : List α) :
    l.filterMap f = l.flatMap fun a ↦ (f a).toList

Proof state:
α : Type u
β : Type v
f : α → Option β
l : List α
⊢ filterMap f l = flatMap (fun a => (f a).toList) l

Tactic:
induction' l with a l ih <;> simp [filterMap_cons]

Result:
case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a => (f a).toList) l
⊢ (match f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (f a).toList ++ flatMap (fun a => (f a).toList) l

Proof state:
case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a => (f a).toList) l
⊢ (match f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (f a).toList ++ flatMap (fun a => (f a).toList) l

Tactic:
rcases f a <;> simp [ih]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem update_lt_self_iff : update x i a < x ↔ a < x i

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a : π i
⊢ update x i a < x ↔ a < x i

Tactic:
simp [lt_iff_le_not_le]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem norm_exp_ofReal (x : ℝ) : ‖exp x‖ = Real.exp x

Proof state:
x : ℝ
⊢ ‖↑(Real.exp x)‖ = Real.exp x

Tactic:
exact Complex.norm_of_nonneg (le_of_lt (Real.exp_pos _))

Result:
no goals

Proof state:
x : ℝ
⊢ ‖cexp ↑x‖ = Real.exp x

Tactic:
rw [← ofReal_exp]

Result:
x : ℝ
⊢ ‖↑(Real.exp x)‖ = Real.exp x