harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Distributions/Pareto.lean
lemma paretoCDFReal_eq_lintegral (ht : 0 < t) (hr : 0 < r) (x : ℝ) :
    cdf (paretoMeasure t r) x = ENNReal.toReal (∫⁻ x in Iic x, paretoPDF t r x)

Proof state:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ ↑(cdf (paretoMeasure t r)) x = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal

Tactic:
rw [cdf_eq_toReal, paretoMeasure, withDensity_apply _ measurableSet_Iic]

Result:
no goals

Proof state:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
⊢ ↑(cdf (paretoMeasure t r)) x = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal

Tactic:
have : IsProbabilityMeasure (paretoMeasure t r) := isProbabilityMeasure_paretoMeasure ht hr

Result:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ ↑(cdf (paretoMeasure t r)) x = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem ball_mul_singleton : ball x δ * {y} = ball (x * y) δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ ball x δ * {y} = ball (x * y) δ

Tactic:
rw [mul_comm, singleton_mul_ball, mul_comm y]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem zero : padicValInt p 0 = 0

Proof state:
p : ℕ
⊢ padicValInt p 0 = 0

Tactic:
simp [padicValInt]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem subset_toFinset {s : Finset α} [Fintype t] : s ⊆ t.toFinset ↔ ↑s ⊆ t

Proof state:
α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ s ⊆ t.toFinset ↔ ↑s ⊆ t

Tactic:
rw [← Finset.coe_subset, coe_toFinset]

Result:
no goals
-- Mathlib/Logic/Hydra.lean
theorem not_cutExpand_zero [IsIrrefl α r] (s) : ¬CutExpand r s 0

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬CutExpand r s 0

Tactic:
rw [cutExpand_iff]

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ 0 ∧ s = erase 0 a + t

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ 0 ∧ s = erase 0 a + t

Tactic:
rintro ⟨_, _, _, ⟨⟩, _⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬CutExpand r s 0

Tactic:
classical
rw [cutExpand_iff]
rintro ⟨_, _, _, ⟨⟩, _⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
lemma exists_inverse {n : ℕ} (c : OrderedFinpartition n) (j : Fin n) :
    ∃ p : Σ m, Fin (c.partSize m), c.emb p.1 p.2 = j

Proof state:
case intro.intro
n : ℕ
c : OrderedFinpartition n
j : Fin n
m : Fin c.length
r : Fin (c.partSize m)
hmr : c.emb m r = j
⊢ ∃ p, c.emb p.fst p.snd = j

Tactic:
exact ⟨⟨m, r⟩, hmr⟩

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition n
j : Fin n
⊢ ∃ p, c.emb p.fst p.snd = j

Tactic:
rcases c.cover j with ⟨m, r, hmr⟩

Result:
case intro.intro
n : ℕ
c : OrderedFinpartition n
j : Fin n
m : Fin c.length
r : Fin (c.partSize m)
hmr : c.emb m r = j
⊢ ∃ p, c.emb p.fst p.snd = j
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@[reassoc (attr := simp)]
lemma lanUnit_app_whiskerLeft_lanAdjunction_counit_app (G : D ⥤ H) :
    L.lanUnit.app (L ⋙ G) ≫ whiskerLeft L ((L.lanAdjunction H).counit.app G) = 𝟙 (L ⋙ G)

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_6, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
G : D ⥤ H
⊢ L.lanUnit.app (L ⋙ G) ≫ whiskerLeft L ((L.lanAdjunction H).counit.app G) = 𝟙 (L ⋙ G)

Tactic:
simp [lanAdjunction_counit_app]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_comm : hausdorffEdist s t = hausdorffEdist t s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ (⨆ x ∈ s, infEdist x t) ⊔ ⨆ y ∈ t, infEdist y s = (⨆ y ∈ t, infEdist y s) ⊔ ⨆ x ∈ s, infEdist x t

Tactic:
apply sup_comm

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist s t = hausdorffEdist t s

Tactic:
simp only [hausdorffEdist_def]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ (⨆ x ∈ s, infEdist x t) ⊔ ⨆ y ∈ t, infEdist y s = (⨆ y ∈ t, infEdist y s) ⊔ ⨆ x ∈ s, infEdist x t
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
theorem exists_sq_eq_two_iff (hp : p ≠ 2) : IsSquare (2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 7

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7

Tactic:
omega

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7

Tactic:
rw [FiniteField.isSquare_two_iff, card p]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7

Tactic:
have h₁ := Prime.mod_two_eq_one_iff_ne_two.mpr hp

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
-- Mathlib/Algebra/Module/PID.lean
theorem Submodule.isInternal_prime_power_torsion_of_pid [DecidableEq (Ideal R)] [Module.Finite R M]
    (hM : Module.IsTorsion R M) :
    DirectSum.IsInternal fun p : (factors (⊤ : Submodule R M).annihilator).toFinset =>
      torsionBy R M
        (IsPrincipal.generator (p : Ideal R) ^
          (factors (⊤ : Submodule R M).annihilator).count ↑p)

Proof state:
case h.e'_8.h
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsPrincipalIdealRing R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
x✝ : { x // x ∈ (factors ⊤.annihilator).toFinset }
⊢ torsionBy R M (IsPrincipal.generator ↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) =
    torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))

Tactic:
ext p : 1

Result:
case h.e'_8.h.h
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsPrincipalIdealRing R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
x✝ : { x // x ∈ (factors ⊤.annihilator).toFinset }
p : M
⊢ p ∈ torsionBy R M (IsPrincipal.generator ↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) ↔
    p ∈ torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))

Proof state:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsPrincipalIdealRing R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal fun p => torsionBy R M (IsPrincipal.generator ↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Tactic:
convert isInternal_prime_power_torsion hM

Result:
case h.e'_8.h
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsPrincipalIdealRing R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
x✝ : { x // x ∈ (factors ⊤.annihilator).toFinset }
⊢ torsionBy R M (IsPrincipal.generator ↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) =
    torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))

Proof state:
case h.e'_8.h.h
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsPrincipalIdealRing R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
x✝ : { x // x ∈ (factors ⊤.annihilator).toFinset }
p : M
⊢ p ∈ torsionBy R M (IsPrincipal.generator ↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) ↔
    p ∈ torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))

Tactic:
rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ← Ideal.span_singleton_pow,
  Ideal.span_singleton_generator]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
    (setIfInBounds a i v)[i]?.getD d = if i < a.size then v else d

Proof state:
α : Type u_1
a : Array α
i : Nat
v d : α
⊢ (a.setIfInBounds i v)[i]?.getD d = if i < a.size then v else d

Tactic:
by_cases h : i < a.size <;>
  simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_getElem?]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_subset_iff_right : image₂ f s t ⊆ u ↔ ∀ b ∈ t, (s.image fun a => f a b) ⊆ u

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ image₂ f s t ⊆ u ↔ ∀ b ∈ t, image (fun a => f a b) s ⊆ u

Tactic:
simp_rw [image₂_subset_iff, image_subset_iff, @forall₂_swap α]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eq_isSome_getValueCast? [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)}
    {a : α} : containsKey a l = (getValueCast? a l).isSome

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a : α
⊢ containsKey a l = (getValueCast? a l).isSome

Tactic:
simp [containsKey_eq_isSome_getEntry?, getValueCast?_eq_getEntry?]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_inf_self (a b : α) : (a ⇨ b) ⊓ a = b ⊓ a

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⇨ b) ⊓ a = b ⊓ a

Tactic:
rw [inf_comm, inf_himp, inf_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSomeRev?_push_of_isNone (l : Vector α n) (h : (f a).isNone) : (l.push a).findSomeRev? f = l.findSomeRev? f

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
a : α
h : (f a).isNone = true
l : Array α
⊢ findSomeRev? f ({ toArray := l, size_toArray := ⋯ }.push a) = findSomeRev? f { toArray := l, size_toArray := ⋯ }

Tactic:
simp only [push_mk, findSomeRev?_mk, Array.findSomeRev?_push_of_isNone, h]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
α✝ : Type u_2
f : α → Option α✝
a : α
l : Vector α n
h : (f a).isNone = true
⊢ findSomeRev? f (l.push a) = findSomeRev? f l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
a : α
h : (f a).isNone = true
l : Array α
⊢ findSomeRev? f ({ toArray := l, size_toArray := ⋯ }.push a) = findSomeRev? f { toArray := l, size_toArray := ⋯ }
-- Mathlib/Topology/Exterior.lean
lemma mem_exterior : x ∈ exterior s ↔ ∀ U, IsOpen U → s ⊆ U → x ∈ U

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ exterior s ↔ ∀ (U : Set X), IsOpen U → s ⊆ U → x ∈ U

Tactic:
simp [exterior_def]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_sub_int (a : α) (z : ℤ) : ⌈a - z⌉ = ⌈a⌉ - z :=
  Eq.trans (by rw [Int.cast_neg, sub_eq_add_neg]) (ceil_add_int _ _)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
z : ℤ
⊢ ⌈a - ↑z⌉ = ⌈a + ↑(-z)⌉

Tactic:
rw [Int.cast_neg, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
lemma expect_apply_eq_ite [Finite α] [DecidableEq α] (a : α) :
    𝔼 ψ : AddChar α ℂ, ψ a = if a = 0 then 1 else 0

Proof state:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : Finite α
inst✝ : DecidableEq α
a : α
⊢ 𝔼 ψ : AddChar α ℂ, ψ a = if a = 0 then 1 else 0

Tactic:
simpa using expect_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma bot_not_connected [Nontrivial V] : ¬(⊥ : SimpleGraph V).Connected

Proof state:
V : Type u
inst✝ : Nontrivial V
⊢ ¬⊥.Connected

Tactic:
simp [bot_not_preconnected, connected_iff, ‹_›]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem exists_of_liftRel_left {R : α → β → Prop} {s t} (H : LiftRel R s t) {a} (h : a ∈ s) :
    ∃ b, b ∈ t ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h : a ∈ s
⊢ ∃ b, b ∈ t ∧ R a b

Tactic:
let ⟨n, h⟩ := exists_get?_of_mem h

Result:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ b, b ∈ t ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ b, b ∈ t ∧ R a b

Tactic:
dsimp only [get?, head] at h

Result:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop n).destruct
⊢ ∃ b, b ∈ t ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop n).destruct
s' : WSeq α
sd : some (a, s') ∈ (s.drop n).destruct
⊢ ∃ b, b ∈ t ∧ R a b

Tactic:
let ⟨some (b, t'), td, ⟨ab, _⟩⟩ := (liftRel_dropn_destruct H n).left sd

Result:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop n).destruct
s' : WSeq α
sd : some (a, s') ∈ (s.drop n).destruct
b : β
t' : WSeq β
td : some (b, t') ∈ (t.drop n).destruct
ab : R a b
right✝ : LiftRel R s' t'
⊢ ∃ b, b ∈ t ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop n).destruct
⊢ ∃ b, b ∈ t ∧ R a b

Tactic:
let ⟨some (_, s'), sd, rfl⟩ := Computation.exists_of_mem_map h

Result:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop n).destruct
s' : WSeq α
sd : some (a, s') ∈ (s.drop n).destruct
⊢ ∃ b, b ∈ t ∧ R a b
-- Mathlib/GroupTheory/Torsion.lean
lemma isTorsionFree_iff_noZeroSMulDivisors_nat {M : Type*} [AddMonoid M] :
    IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M

Proof state:
M : Type u_3
inst✝ : AddMonoid M
⊢ (∀ (y : ℕ) (x : M), x ≠ 0 → y ≠ 0 → ¬y • x = 0) ↔ ∀ {c : ℕ} {x : M}, c • x = 0 → c = 0 ∨ x = 0

Tactic:
exact forall₂_congr fun _ _ ↦ by tauto

Result:
no goals

Proof state:
M : Type u_3
inst✝ : AddMonoid M
x✝¹ : ℕ
x✝ : M
⊢ x✝ ≠ 0 → x✝¹ ≠ 0 → ¬x✝¹ • x✝ = 0 ↔ x✝¹ • x✝ = 0 → x✝¹ = 0 ∨ x✝ = 0

Tactic:
tauto

Result:
no goals

Proof state:
M : Type u_3
inst✝ : AddMonoid M
⊢ IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M

Tactic:
simp_rw [AddMonoid.IsTorsionFree, isOfFinAddOrder_iff_nsmul_eq_zero, not_exists, not_and,
  pos_iff_ne_zero, noZeroSMulDivisors_iff, forall_swap (β := ℕ)]

Result:
M : Type u_3
inst✝ : AddMonoid M
⊢ (∀ (y : ℕ) (x : M), x ≠ 0 → y ≠ 0 → ¬y • x = 0) ↔ ∀ {c : ℕ} {x : M}, c • x = 0 → c = 0 ∨ x = 0
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
lemma _root_.Real.lipschitzWith_toNNReal : LipschitzWith 1 Real.toNNReal

Proof state:
⊢ LipschitzWith 1 Real.toNNReal

Tactic:
refine lipschitzWith_iff_dist_le_mul.mpr (fun x y ↦ ?_)

Result:
x y : ℝ
⊢ dist x.toNNReal y.toNNReal ≤ ↑1 * dist x y

Proof state:
x y : ℝ
⊢ dist x.toNNReal y.toNNReal ≤ ↑1 * dist x y

Tactic:
simpa only [NNReal.coe_one, dist_prod_same_right, one_mul, Real.dist_eq] using
  lipschitzWith_iff_dist_le_mul.mp lipschitzWith_max (x, 0) (y, 0)

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Algebra.isAlgebraic_of_not_injective (h : ¬ Function.Injective (algebraMap R A)) :
    Algebra.IsAlgebraic R A where
  isAlgebraic a := isAlgebraic_iff_not_injective.mpr
    fun inj ↦ h <| by convert inj.comp C_injective; ext; simp

Proof state:
case h.e'_3
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Function.Injective ⇑(algebraMap R A)
a : A
inj : Function.Injective ⇑(aeval a)
⊢ ⇑(algebraMap R A) = ⇑(aeval a) ∘ ⇑C

Tactic:
ext

Result:
case h.e'_3.h
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Function.Injective ⇑(algebraMap R A)
a : A
inj : Function.Injective ⇑(aeval a)
x✝ : R
⊢ (algebraMap R A) x✝ = (⇑(aeval a) ∘ ⇑C) x✝

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Function.Injective ⇑(algebraMap R A)
a : A
inj : Function.Injective ⇑(aeval a)
⊢ Function.Injective ⇑(algebraMap R A)

Tactic:
convert inj.comp C_injective

Result:
case h.e'_3
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Function.Injective ⇑(algebraMap R A)
a : A
inj : Function.Injective ⇑(aeval a)
⊢ ⇑(algebraMap R A) = ⇑(aeval a) ∘ ⇑C

Proof state:
case h.e'_3.h
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Function.Injective ⇑(algebraMap R A)
a : A
inj : Function.Injective ⇑(aeval a)
x✝ : R
⊢ (algebraMap R A) x✝ = (⇑(aeval a) ∘ ⇑C) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_eq_of_sin_eq {x y : ℝ} (h₁ : sin x = y) (h₂ : x ∈ Icc (-(π / 2)) (π / 2)) :
    arcsin y = x

Proof state:
x y : ℝ
h₁ : sin x = y
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin y = x

Tactic:
subst y

Result:
x : ℝ
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin (sin x) = x

Proof state:
x : ℝ
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin (sin x) = x

Tactic:
exact injOn_sin (arcsin_mem_Icc _) h₂ (sin_arcsin' (sin_mem_Icc x))

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp] lemma height_bot (α : Type*) [Preorder α] [OrderBot α] : height (⊥ : α) = 0

Proof state:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ height ⊥ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem find?_some_mem_toList {t : RBMap α β cmp} (h : t.find? x = some v) :
    ∃ y, (y, v) ∈ toList t ∧ cmp x y = .eq

Proof state:
case intro.mk.intro
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
y : α
v : β
h' : t.findEntry? x = some (y, v)
h : t.find? x = some (y, v).snd
⊢ ∃ y_1, (y_1, (y, v).snd) ∈ t.toList ∧ cmp x y_1 = Ordering.eq

Tactic:
exact ⟨_, findEntry?_some_mem_toList h', findEntry?_some_eq_eq h'⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
v : β
t : RBMap α β cmp
h : t.find? x = some v
⊢ ∃ y, (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq

Tactic:
obtain ⟨⟨y, v⟩, h', rfl⟩ := Option.map_eq_some'.1 h

Result:
case intro.mk.intro
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
y : α
v : β
h' : t.findEntry? x = some (y, v)
h : t.find? x = some (y, v).snd
⊢ ∃ y_1, (y_1, (y, v).snd) ∈ t.toList ∧ cmp x y_1 = Ordering.eq
-- Mathlib/Topology/Algebra/Support.lean
@[to_additive, simp]
protected lemma HasCompactMulSupport.one {α β : Type*} [TopologicalSpace α] [One β] :
    HasCompactMulSupport (1 : α → β)

Proof state:
α : Type u_9
β : Type u_10
inst✝¹ : TopologicalSpace α
inst✝ : One β
⊢ HasCompactMulSupport 1

Tactic:
simp [HasCompactMulSupport, mulTSupport]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderiv_zero_of_not_mdifferentiableAt (h : ¬MDifferentiableAt I I' f x) :
    mfderiv I I' f x = 0

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
h : ¬MDifferentiableAt I I' f x
⊢ mfderiv I I' f x = 0

Tactic:
simp only [mfderiv, h, if_neg, not_false_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
@[simp]
lemma coroot_apply_self : coroot B hx x = 2 :=
  hx.regular.left <| by simp [mul_comm _ (B x x)]

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
⊢ (fun x_1 => (B x) x * x_1) ((coroot B hx) x) = (fun x_1 => (B x) x * x_1) 2

Tactic:
simp [mul_comm _ (B x x)]

Result:
no goals
-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem dist_mem_candidates :
    (fun p : (X ⊕ Y) × (X ⊕ Y) => dist p.1 p.2) ∈ candidates X Y

Proof state:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
⊢ (fun p => dist p.1 p.2) ∈ candidates X Y

Tactic:
simp_rw [candidates, Set.mem_setOf_eq, dist_comm, dist_triangle, dist_self, maxVar_bound,
  forall_const, and_true]

Result:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
⊢ (∀ (x y : X), dist (inl x) (inl y) = dist x y) ∧ ∀ (x y : Y), dist (inr x) (inr y) = dist x y

Proof state:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
⊢ (∀ (x y : X), dist (inl x) (inl y) = dist x y) ∧ ∀ (x y : Y), dist (inr x) (inr y) = dist x y

Tactic:
exact ⟨fun x y => rfl, fun x y => rfl⟩

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.pre_pre [h : HasLimit (D ⋙ E ⋙ F)] : haveI : HasLimit ((D ⋙ E) ⋙ F) := h
    limit.pre F E ≫ limit.pre (E ⋙ F) D = limit.pre F (D ⋙ E)

Proof state:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimit F
E : K ⥤ J
inst✝¹ : HasLimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ π F (E.obj (D.obj j)) = π F ((D ⋙ E).obj j)

Tactic:
rfl

Result:
no goals

Proof state:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimit F
E : K ⥤ J
inst✝¹ : HasLimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ (pre F E ≫ pre (E ⋙ F) D) ≫ π (D ⋙ E ⋙ F) j = pre F (D ⋙ E) ≫ π (D ⋙ E ⋙ F) j

Tactic:
erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]

Result:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimit F
E : K ⥤ J
inst✝¹ : HasLimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ π F (E.obj (D.obj j)) = π F ((D ⋙ E).obj j)

Proof state:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimit F
E : K ⥤ J
inst✝¹ : HasLimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
⊢ pre F E ≫ pre (E ⋙ F) D = pre F (D ⋙ E)

Tactic:
ext j

Result:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimit F
E : K ⥤ J
inst✝¹ : HasLimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ (pre F E ≫ pre (E ⋙ F) D) ≫ π (D ⋙ E ⋙ F) j = pre F (D ⋙ E) ≫ π (D ⋙ E ⋙ F) j

Proof state:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimit F
E : K ⥤ J
inst✝¹ : HasLimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
⊢ pre F E ≫ pre (E ⋙ F) D = pre F (D ⋙ E)

Tactic:
haveI : HasLimit ((D ⋙ E) ⋙ F) := h

Result:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimit F
E : K ⥤ J
inst✝¹ : HasLimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
⊢ pre F E ≫ pre (E ⋙ F) D = pre F (D ⋙ E)
-- Mathlib/Data/Real/Hyperreal.lean
theorem Infinitesimal.neg {x : ℝ*} (hx : Infinitesimal x) : Infinitesimal (-x)

Proof state:
x : ℝ*
hx : x.Infinitesimal
⊢ (-x).Infinitesimal

Tactic:
simpa only [neg_zero] using hx.neg

Result:
no goals