harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem witt_structure_prop (Φ : MvPolynomial idx ℤ) (n) :
    aeval (fun i => map (Int.castRingHom R) (wittStructureInt p Φ i)) (wittPolynomial p ℤ n) =
      aeval (fun i => rename (Prod.mk i) (W n)) Φ

Proof state:
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => (map (Int.castRingHom R)) (wittStructureInt p Φ i)) = fun i =>
    (map (Int.castRingHom R)) (wittStructureInt p Φ i)

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => (rename (Prod.mk i)) (W_ R n)) = fun i => (map (Int.castRingHom R)) ((rename (Prod.mk i)) (W_ ℤ n))

Tactic:
simp only [map_rename, map_wittPolynomial]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i => (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    (aeval fun i => (rename (Prod.mk i)) (W_ R n)) Φ

Tactic:
convert congr_arg (map (Int.castRingHom R)) (wittStructureInt_prop p Φ n) using 1 <;>
    rw [hom_bind₁] <;>
  apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl

Result:
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => (map (Int.castRingHom R)) (wittStructureInt p Φ i)) = fun i =>
    (map (Int.castRingHom R)) (wittStructureInt p Φ i)

p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => (rename (Prod.mk i)) (W_ R n)) = fun i => (map (Int.castRingHom R)) ((rename (Prod.mk i)) (W_ ℤ n))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem hasPos_addNeg (assignment : Assignment) :
    hasPosAssignment (addNegAssignment assignment) = hasPosAssignment assignment

Proof state:
assignment : Assignment
⊢ assignment.addNegAssignment.hasPosAssignment = assignment.hasPosAssignment

Tactic:
cases assignment <;> simp [hasPosAssignment, addNegAssignment]

Result:
no goals
-- Mathlib/Algebra/Order/Nonneg/Basic.lean
theorem toNonneg_of_nonneg {a : α} (h : 0 ≤ a) : toNonneg a = ⟨a, h⟩

Proof state:
α : Type u_1
inst✝¹ : Zero α
inst✝ : SemilatticeSup α
a : α
h : 0 ≤ a
⊢ toNonneg a = ⟨a, h⟩

Tactic:
simp [toNonneg, h]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_eq_empty {α β} {f : α → β} {s : Set α} : f '' s = ∅ ↔ s = ∅

Proof state:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ (∀ (x : β), x ∉ f '' s) ↔ ∀ (x : α), x ∉ s

Tactic:
exact ⟨fun H a ha => H _ ⟨_, ha, rfl⟩, fun H b ⟨_, ha, _⟩ => H _ ha⟩

Result:
no goals

Proof state:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ f '' s = ∅ ↔ s = ∅

Tactic:
simp only [eq_empty_iff_forall_not_mem]

Result:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ (∀ (x : β), x ∉ f '' s) ↔ ∀ (x : α), x ∉ s
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem writtenInExtChartAt_chartAt_symm {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt I I (chartAt H x x) (chartAt H x).symm y = y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
h : y ∈ (extChartAt I x).target
⊢ writtenInExtChartAt I I (↑(chartAt H x) x) (↑(chartAt H x).symm) y = y

Tactic:
simp_all only [mfld_simps]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem csInf_image_le {s : Set α} {c : α} (hcs : c ∈ s) (h_bdd : BddBelow s) :
    sInf (f '' s) ≤ f c

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
c : α
hcs : c ∈ s
h_bdd : BddBelow s
⊢ sInf (f '' s) ≤ f c

Tactic:
let f' : αᵒᵈ → βᵒᵈ := f

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
c : α
hcs : c ∈ s
h_bdd : BddBelow s
f' : αᵒᵈ → βᵒᵈ := f
⊢ sInf (f '' s) ≤ f c

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
c : α
hcs : c ∈ s
h_bdd : BddBelow s
f' : αᵒᵈ → βᵒᵈ := f
⊢ sInf (f '' s) ≤ f c

Tactic:
exact le_csSup_image (α := αᵒᵈ) (β := βᵒᵈ)
  (show Monotone f' from fun x y hxy => h_mono hxy) hcs h_bdd

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_isEmpty [IsEmpty n] {A : Matrix n n R} : det A = 1

Proof state:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : IsEmpty n
A : Matrix n n R
⊢ A.det = 1

Tactic:
simp [det_apply]

Result:
no goals
-- Mathlib/Order/Category/Preord.lean
lemma comp_apply {X Y Z : Preord} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : Preord
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive (attr := simp) mod_natCard_nsmul]
lemma pow_mod_natCard {G} [Group G] (a : G) (n : ℕ) : a ^ (n % Nat.card G) = a ^ n

Proof state:
G : Type u_6
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (n % Nat.card G) = a ^ n

Tactic:
rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n <| orderOf_dvd_natCard _, pow_mod_orderOf]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem right_ne_zero_of_oangle_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : y ≠ 0 :=
  o.right_ne_zero_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 1
⊢ 1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithBot.ofDual_le_iff {x : WithBot αᵒᵈ} {y : WithTop α} :
    WithBot.ofDual x ≤ y ↔ y.toDual ≤ x

Proof state:
α : Type u_1
inst✝ : LE α
x : WithBot αᵒᵈ
y : WithTop α
⊢ WithBot.ofDual x ≤ y ↔ WithTop.toDual y ≤ x

Tactic:
cases x <;> cases y <;> simp [toDual_le]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_p_pow (n : ℕ) : ‖(p : ℤ_[p]) ^ n‖ = (p : ℝ) ^ (-n : ℤ)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑p ^ n‖ = ↑p ^ (-↑n)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Category/Stonean/Basic.lean
@[simp, reassoc]
lemma lift_lifts {X Y : Profinite} {Z : Stonean} (e : Stonean.toProfinite.obj Z ⟶ Y) (f : X ⟶ Y)
    [Epi f] : lift e f ≫ f = e

Proof state:
X Y : Profinite
Z : Stonean
e : Stonean.toProfinite.obj Z ⟶ Y
f : X ⟶ Y
inst✝ : Epi f
⊢ lift e f ≫ f = e

Tactic:
simp [lift]

Result:
no goals
-- Mathlib/GroupTheory/CommutingProbability.lean
@[simp] lemma reciprocalFactors_one : reciprocalFactors 1 = []

Proof state:
⊢ (if x : 1 = 0 then [0]
    else
      if x : 1 = 1 then []
      else if Even 1 then 3 :: reciprocalFactors (1 / 2) else 1 % 4 * 1 :: reciprocalFactors (1 / 4 + 1)) =
    []

Tactic:
rfl

Result:
no goals

Proof state:
⊢ reciprocalFactors 1 = []

Tactic:
unfold reciprocalFactors

Result:
⊢ (if x : 1 = 0 then [0]
    else
      if x : 1 = 1 then []
      else if Even 1 then 3 :: reciprocalFactors (1 / 2) else 1 % 4 * 1 :: reciprocalFactors (1 / 4 + 1)) =
    []
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem linearIndependent_iff_smaller (o : Ordinal) :
    LinearIndependent ℤ (GoodProducts.eval (π C (ord I · < o))) ↔
    LinearIndependent ℤ (fun (p : smaller C o) ↦ p.1)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ LinearIndependent ℤ (eval (π C fun x => ord I x < o)) ↔ LinearIndependent ℤ fun (p : ↑(smaller C o)) => ↑p

Tactic:
rw [GoodProducts.linearIndependent_iff_range,
  ← LinearMap.linearIndependent_iff (πs C o)
  (LinearMap.ker_eq_bot_of_injective (injective_πs _ _)), ← smaller_factorization C o]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ LinearIndependent (ι := ↑(range (π C fun x => ord I x < o))) ℤ ((fun p => ↑p) ∘ (range_equiv_smaller C o).toFun) ↔
    LinearIndependent ℤ fun (p : ↑(smaller C o)) => ↑p

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ LinearIndependent (ι := ↑(range (π C fun x => ord I x < o))) ℤ ((fun p => ↑p) ∘ (range_equiv_smaller C o).toFun) ↔
    LinearIndependent ℤ fun (p : ↑(smaller C o)) => ↑p

Tactic:
exact linearIndependent_equiv _

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem isNormal_opow {a : Ordinal} (h : 1 < a) : IsNormal (a ^ ·) :=
  have a0 : 0 < a := zero_lt_one.trans h
  ⟨fun b => by simpa only [mul_one, opow_succ] using (mul_lt_mul_iff_left (opow_pos b a0)).2 h,
    fun _ l _ => opow_le_of_limit (ne_of_gt a0) l⟩

Proof state:
a : Ordinal.{u_1}
h : 1 < a
a0 : 0 < a
b : Ordinal.{u_1}
⊢ (fun x => a ^ x) b < (fun x => a ^ x) (succ b)

Tactic:
simpa only [mul_one, opow_succ] using (mul_lt_mul_iff_left (opow_pos b a0)).2 h

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem codisjoint_hnot_hnot_right_iff : Codisjoint a (￢￢b) ↔ Codisjoint a b

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint a (￢￢b) ↔ Codisjoint a b

Tactic:
simp_rw [← hnot_le_iff_codisjoint_left, hnot_hnot_hnot]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem lt_opow_of_limit {a b c : Ordinal} (b0 : b ≠ 0) (h : IsLimit c) :
    a < b ^ c ↔ ∃ c' < c, a < b ^ c'

Proof state:
a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : c.IsLimit
⊢ ¬a < b ^ c ↔ ∀ (x : Ordinal.{u_1}), ¬(x < c ∧ a < b ^ x)

Tactic:
simp only [not_lt, opow_le_of_limit b0 h, exists_prop, not_and]

Result:
no goals

Proof state:
a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : c.IsLimit
⊢ a < b ^ c ↔ ∃ c' < c, a < b ^ c'

Tactic:
rw [← not_iff_not, not_exists]

Result:
a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : c.IsLimit
⊢ ¬a < b ^ c ↔ ∀ (x : Ordinal.{u_1}), ¬(x < c ∧ a < b ^ x)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    {fallback : β a} (hl : DistinctKeys l) : getValueCastD a (eraseKey k l) fallback =
      if k == a then fallback else getValueCastD a l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
fallback : β a
hl : DistinctKeys l
⊢ getValueCastD a (eraseKey k l) fallback = if (k == a) = true then fallback else getValueCastD a l fallback

Tactic:
simp [getValueCastD_eq_getValueCast?, getValueCast?_eraseKey hl,
  apply_ite (fun x => Option.getD x fallback)]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
lemma isIso_of_isIso {X Y : T} {f : X ⟶ Y} {g : Arrow T} (sq : mk f ⟶ g) [IsIso sq] [IsIso f] :
    IsIso g.hom

Proof state:
T : Type u
inst✝² : Category.{v, u} T
X Y : T
f : X ⟶ Y
g : Arrow T
sq : mk f ⟶ g
inst✝¹ : IsIso sq
inst✝ : IsIso f
⊢ IsIso ((asIso sq).inv.left ≫ f ≫ (asIso sq).hom.right)

Tactic:
infer_instance

Result:
no goals

Proof state:
T : Type u
inst✝² : Category.{v, u} T
X Y : T
f : X ⟶ Y
g : Arrow T
sq : mk f ⟶ g
inst✝¹ : IsIso sq
inst✝ : IsIso f
⊢ IsIso g.hom

Tactic:
rw [iso_w' (asIso sq)]

Result:
T : Type u
inst✝² : Category.{v, u} T
X Y : T
f : X ⟶ Y
g : Arrow T
sq : mk f ⟶ g
inst✝¹ : IsIso sq
inst✝ : IsIso f
⊢ IsIso ((asIso sq).inv.left ≫ f ≫ (asIso sq).hom.right)
-- Mathlib/ModelTheory/Fraisse.lean
theorem isFraisse_finite : IsFraisse { S : Bundled.{w} Language.empty.Structure | Finite S }

Proof state:
⊢ IsFraisse {S | Finite ↑S}

Tactic:
have : Language.empty.Structure (ULift ℕ : Type w) := emptyStructure

Result:
this : Language.empty.Structure (ULift.{w, 0} ℕ)
⊢ IsFraisse {S | Finite ↑S}

Proof state:
this : Language.empty.Structure (ULift.{w, 0} ℕ)
⊢ IsFraisse {S | Finite ↑S}

Tactic:
exact (isFraisseLimit_of_countable_infinite (ULift ℕ)).isFraisse

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma gaussianPDF_pos (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) (x : ℝ) : 0 < gaussianPDF μ v x

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ 0 < gaussianPDFReal μ v x

Tactic:
exact gaussianPDFReal_pos _ _ _ hv

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ 0 < gaussianPDF μ v x

Tactic:
rw [gaussianPDF, ENNReal.ofReal_pos]

Result:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ 0 < gaussianPDFReal μ v x
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIcc_comm (a b : α) : [[a, b]] = [[b, a]]

Proof state:
α : Type u_1
inst✝ : Lattice α
a b : α
⊢ [[a, b]] = [[b, a]]

Tactic:
simp_rw [uIcc, inf_comm, sup_comm]

Result:
no goals
-- Mathlib/Data/Finset/Defs.lean
theorem not_subset : ¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t

Proof state:
α : Type u_1
s t : Finset α
⊢ ¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t

Tactic:
simp only [← coe_subset, Set.not_subset, mem_coe]

Result:
no goals
-- Mathlib/Topology/Clopen.lean
lemma IsClopen.himp (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ⇨ t)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClopen s
ht : IsClopen t
⊢ IsClopen (s ⇨ t)

Tactic:
simpa [himp_eq] using ht.union hs.compl

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem terminatedAt_map_iff {f : α → β} {s : Seq α} {n : ℕ} :
    (map f s).TerminatedAt n ↔ s.TerminatedAt n

Proof state:
α : Type u
β : Type v
f : α → β
s : Seq α
n : ℕ
⊢ (map f s).TerminatedAt n ↔ s.TerminatedAt n

Tactic:
simp [TerminatedAt]

Result:
no goals
-- Mathlib/Data/Sum/Interval.lean
lemma inr_mem_sumLexLift {c₂ : γ₂} :
    inr c₂ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
      (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ f₂ a₂ b₂

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ inr c₂ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
simp [mem_sumLexLift]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem zpow_eq_zpow_iff_modEq {m n : ℤ} : x ^ m = x ^ n ↔ m ≡ n [ZMOD orderOf x]

Proof state:
G : Type u_1
inst✝ : Group G
x : G
m n : ℤ
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD ↑(orderOf x)]

Tactic:
rw [← mul_inv_eq_one, ← zpow_sub, zpow_eq_one_iff_modEq, Int.modEq_iff_dvd, Int.modEq_iff_dvd,
  zero_sub, neg_sub]

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Icc_pred_right_eq_Ico_of_not_isMin (hb : ¬ IsMin b) (a : α) : Icc a (pred b) = Ico a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (pred b) = Ico a b

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a x : α
⊢ x ∈ Icc a (pred b) ↔ x ∈ Ico a b

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a x : α
⊢ x ∈ Icc a (pred b) ↔ x ∈ Ico a b

Tactic:
rw [mem_Icc, mem_Ico, le_pred_iff_of_not_isMin hb]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem contDiffAt_ring_inverse [HasSummableGeomSeries R] (x : Rˣ) :
    ContDiffAt 𝕜 n Ring.inverse (x : R)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
R : Type u_3
inst✝² : NormedRing R
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ ContDiffAt 𝕜 n Ring.inverse ↑x

Tactic:
have := AnalyticOnNhd.contDiffOn (analyticOnNhd_inverse (𝕜 := 𝕜) (A := R)) (n := n)
  Units.isOpen.uniqueDiffOn x x.isUnit

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
R : Type u_3
inst✝² : NormedRing R
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : HasSummableGeomSeries R
x : Rˣ
this : ContDiffWithinAt 𝕜 n Ring.inverse {x | IsUnit x} ↑x
⊢ ContDiffAt 𝕜 n Ring.inverse ↑x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
R : Type u_3
inst✝² : NormedRing R
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : HasSummableGeomSeries R
x : Rˣ
this : ContDiffWithinAt 𝕜 n Ring.inverse {x | IsUnit x} ↑x
⊢ ContDiffAt 𝕜 n Ring.inverse ↑x

Tactic:
exact this.contDiffAt (Units.isOpen.mem_nhds x.isUnit)

Result:
no goals
-- Mathlib/Order/Sublattice.lean
@[simp] lemma pi_bot {s : Set κ} (hs : s.Nonempty) : (pi s fun _ ↦ ⊥ : Sublattice (∀ i, π i)) = ⊥ :=
  ext fun a ↦ by simpa [mem_pi] using hs

Proof state:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
hs : s.Nonempty
a : (i : κ) → π i
⊢ (a ∈ pi s fun x => ⊥) ↔ a ∈ ⊥

Tactic:
simpa [mem_pi] using hs

Result:
no goals
-- Mathlib/Tactic/NormNum/RealSqrt.lean
lemma isNat_realSqrt {x : ℝ} {nx ny : ℕ} (h : IsNat x nx) (hy : ny * ny = nx) :
    IsNat √x ny := ⟨by simp [h.out, ← hy]⟩

Proof state:
x : ℝ
nx ny : ℕ
h : IsNat x nx
hy : ny * ny = nx
⊢ √x = ↑ny

Tactic:
simp [h.out, ← hy]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_le_one_iff {a : Cardinal.{u}} :
    lift.{v} a ≤ 1 ↔ a ≤ 1

Proof state:
a : Cardinal.{u}
⊢ lift.{v, u} a ≤ 1 ↔ a ≤ 1

Tactic:
simpa using lift_le_nat_iff (n := 1)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem norm_integral_eq_norm_integral_Ioc (f : ℝ → E) :
    ‖∫ x in a..b, f x ∂μ‖ = ‖∫ x in Ι a b, f x ∂μ‖

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
⊢ ‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖

Tactic:
rw [← norm_integral_min_max, integral_of_le min_le_max, uIoc]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem HasProd.sigma_of_hasProd {γ : β → Type*} {f : (Σb : β, γ b) → α} {g : β → α}
    {a : α} (ha : HasProd g a) (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) (hf' : Multipliable f) :
    HasProd f a

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : T3Space α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd g a
hf : ∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)
hf' : Multipliable f
⊢ HasProd f a

Tactic:
simpa [(hf'.hasProd.sigma hf).unique ha] using hf'.hasProd

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_finsupp_self (ι : Type w) : Module.rank R (ι →₀ R) = Cardinal.lift.{u} #ι

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
ι : Type w
⊢ Module.rank R (ι →₀ R) = lift.{u, w} #ι

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Exterior.lean
lemma subset_exterior_iff : s ⊆ exterior t ↔ ∀ U, IsOpen U → t ⊆ U → s ⊆ U

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

Tactic:
simp [exterior_def]

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem factorMultiset_one : factorMultiset 1 = 0

Proof state:
⊢ factorMultiset 1 = 0

Tactic:
simp [factorMultiset, PrimeMultiset.ofNatList, PrimeMultiset.ofNatMultiset]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
theorem biUnion_lt_ball (x : α) (r : ℝ) : ⋃ r' < r, ball x r' = ball x r

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋃ r', ⋃ (_ : r' < r), ball x r' = ball x r

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋃ r', ⋃ (_ : r' < r), ball x r' ↔ x✝ ∈ ball x r

Proof state:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋃ r', ⋃ (_ : r' < r), ball x r' ↔ x✝ ∈ ball x r

Tactic:
rw [← not_iff_not]

Result:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), ball x r' ↔ x✝ ∉ ball x r

Proof state:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), ball x r' ↔ x✝ ∉ ball x r

Tactic:
simp [forall_lt_imp_le_iff_le_of_dense]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
lemma index_extendMiddle_zero (c : OrderedFinpartition n) (i : Fin c.length) :
    (c.extendMiddle i).index 0 = i

Proof state:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this :
  (c.extendMiddle i).emb i 0 = (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)
⊢ (c.extendMiddle i).index 0 = i

Tactic:
contrapose! this

Result:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : ¬(c.extendMiddle i).index 0 = i
⊢ ¬(c.extendMiddle i).emb i 0 = (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)

Proof state:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
⊢ (c.extendMiddle i).index 0 = i

Tactic:
have : (c.extendMiddle i).emb i 0 = 0 := by simp [extendMiddle]

Result:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : (c.extendMiddle i).emb i 0 = 0
⊢ (c.extendMiddle i).index 0 = i

Proof state:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : ¬(c.extendMiddle i).index 0 = i
⊢ ¬(c.extendMiddle i).emb i 0 = (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)

Tactic:
exact (c.extendMiddle i).emb_ne_emb_of_ne (Ne.symm this)

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : (c.extendMiddle i).emb i 0 = 0
⊢ (c.extendMiddle i).index 0 = i

Tactic:
conv_rhs at this => rw [← (c.extendMiddle i).emb_invEmbedding 0]

Result:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this :
  (c.extendMiddle i).emb i 0 = (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)
⊢ (c.extendMiddle i).index 0 = i

Proof state:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
⊢ (c.extendMiddle i).emb i 0 = 0

Tactic:
simp [extendMiddle]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma coroot_root_two :
    P.toLin.flip (P.coroot i) (P.root i) = 2

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (P.toLin.flip (P.coroot i)) (P.root i) = 2

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_id_fun' {α : Type u} : Option.map (fun (a : α) => a) = id

Proof state:
case h
α : Type u
x✝ : Option α
⊢ Option.map (fun a => a) x✝ = id x✝

Tactic:
simp [map_id']

Result:
no goals

Proof state:
α : Type u
⊢ (Option.map fun a => a) = id

Tactic:
funext

Result:
case h
α : Type u
x✝ : Option α
⊢ Option.map (fun a => a) x✝ = id x✝
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integrableOn_Ioi_deriv_of_nonneg' (hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x)
    (g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x) (hg : Tendsto g atTop (𝓝 l)) : IntegrableOn g' (Ioi a)

Proof state:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousWithinAt g (Ici a) a

Tactic:
exact (hderiv a left_mem_Ici).continuousAt.continuousWithinAt

Result:
no goals

Proof state:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a) volume

Tactic:
refine integrableOn_Ioi_deriv_of_nonneg ?_ (fun x hx => hderiv x hx.out.le) g'pos hg

Result:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousWithinAt g (Ici a) a