harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem _root_.RingHom.map_adjugate {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S)
    (M : Matrix n n R) : f.mapMatrix M.adjugate = Matrix.adjugate (f.mapMatrix M)

Proof state:
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i 1 = ⇑f ∘ Pi.single i 1

Tactic:
rw [← f.map_one]

Result:
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i (f 1) = ⇑f ∘ Pi.single i 1

Proof state:
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
⊢ f.mapMatrix M.adjugate = (f.mapMatrix M).adjugate

Tactic:
ext i k

Result:
case a
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ f.mapMatrix M.adjugate i k = (f.mapMatrix M).adjugate i k

Proof state:
case a
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ f.mapMatrix M.adjugate i k = (f.mapMatrix M).adjugate i k

Tactic:
have : Pi.single i (1 : S) = f ∘ Pi.single i 1 := by
  rw [← f.map_one]
  exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)

Result:
case a
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ⇑f ∘ Pi.single i 1
⊢ f.mapMatrix M.adjugate i k = (f.mapMatrix M).adjugate i k

Proof state:
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i (f 1) = ⇑f ∘ Pi.single i 1

Tactic:
exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)

Result:
no goals

Proof state:
case a
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ⇑f ∘ Pi.single i 1
⊢ f.mapMatrix M.adjugate i k = (f.mapMatrix M).adjugate i k

Tactic:
rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
  map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem frobeniusEquiv_symm_comp_frobenius :
    ((frobeniusEquiv R p).symm : R →+* R).comp (frobenius R p) = RingHom.id R

Proof state:
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (↑(frobeniusEquiv R p).symm).comp (frobenius R p) = RingHom.id R

Tactic:
ext

Result:
case a
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x✝ : R
⊢ ((↑(frobeniusEquiv R p).symm).comp (frobenius R p)) x✝ = (RingHom.id R) x✝

Proof state:
case a
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x✝ : R
⊢ ((↑(frobeniusEquiv R p).symm).comp (frobenius R p)) x✝ = (RingHom.id R) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem infinite_odd_deficient : {n : ℕ | Odd n ∧ n.Deficient}.Infinite

Proof state:
n p : ℕ
left✝ : (n + 1) ⊔ 3 ≤ p
h2 : Prime p
⊢ n < p

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
⊢ ∃ b ∈ {n | Odd n ∧ n.Deficient}, n < b

Tactic:
obtain ⟨p, ⟨_, h2⟩⟩ := exists_infinite_primes (max (n + 1) 3)

Result:
case intro.intro
n p : ℕ
left✝ : (n + 1) ⊔ 3 ≤ p
h2 : Prime p
⊢ ∃ b ∈ {n | Odd n ∧ n.Deficient}, n < b

Proof state:
n p : ℕ
left✝ : (n + 1) ⊔ 3 ≤ p
h2 : Prime p
⊢ 2 < p

Tactic:
omega

Result:
no goals

Proof state:
⊢ {n | Odd n ∧ n.Deficient}.Infinite

Tactic:
rw [Set.infinite_iff_exists_gt]

Result:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Odd n ∧ n.Deficient}, a < b

Proof state:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Odd n ∧ n.Deficient}, a < b

Tactic:
intro n

Result:
n : ℕ
⊢ ∃ b ∈ {n | Odd n ∧ n.Deficient}, n < b

Proof state:
case intro.intro
n p : ℕ
left✝ : (n + 1) ⊔ 3 ≤ p
h2 : Prime p
⊢ ∃ b ∈ {n | Odd n ∧ n.Deficient}, n < b

Tactic:
exact ⟨p, Set.mem_setOf.mpr ⟨Prime.odd_of_ne_two h2 (Ne.symm (ne_of_lt (by omega))),
  Prime.deficient h2⟩, by omega⟩

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean
theorem Sphere.secondInter_eq_self_iff {s : Sphere P} {p : P} {v : V} :
    s.secondInter p v = p ↔ ⟪v, p -ᵥ s.center⟫ = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : -2 = 0 ∨ inner v (p -ᵥ s.center) = 0
hv : ¬v = 0
⊢ -2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : inner v (p -ᵥ s.center) = 0
⊢ s.secondInter p v = p

Tactic:
rw [Sphere.secondInter, hp, mul_zero, zero_div, zero_smul, zero_vadd]

Result:
no goals

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
⊢ inner v (p -ᵥ s.center) = 0

Tactic:
rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
  or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
  or_iff_right (by norm_num : (-2 : ℝ) ≠ 0)] at hp

Result:
no goals

Proof state:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
⊢ inner v (p -ᵥ s.center) = 0

Tactic:
by_cases hv : v = 0

Result:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : v = 0
⊢ inner v (p -ᵥ s.center) = 0

case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
⊢ inner v (p -ᵥ s.center) = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ s.secondInter p v = p ↔ inner v (p -ᵥ s.center) = 0

Tactic:
refine ⟨fun hp => ?_, fun hp => ?_⟩

Result:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
⊢ inner v (p -ᵥ s.center) = 0

case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : inner v (p -ᵥ s.center) = 0
⊢ s.secondInter p v = p

Proof state:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : v = 0
⊢ inner v (p -ᵥ s.center) = 0

Tactic:
simp [hv]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
lemma monovaryOn_iff_forall_smul_nonneg :
    MonovaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ (∀ x ∈ s, ∀ x_2 ∈ s, f x < f x_2 → g x ≤ g x_2) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, g x < g x_2 → f x ≤ f x_2

Tactic:
exact (and_iff_right_of_imp MonovaryOn.symm).symm

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)

Tactic:
simp_rw [smul_nonneg_iff_pos_imp_nonneg, sub_pos, sub_nonneg, forall_and]

Result:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ (∀ x ∈ s, ∀ x_2 ∈ s, f x < f x_2 → g x ≤ g x_2) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, g x < g x_2 → f x ≤ f x_2
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem parentD_findAux_rootD {self : UnionFind} {x : Fin self.size} :
    parentD (findAux self x).s (self.rootD x) = self.rootD x

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s (self.rootD self.arr[↑x].parent) = self.rootD self.arr[↑x].parent

Tactic:
exact parentD_findAux_rootD (x := ⟨_, self.parent'_lt _ x.2⟩)

Result:
no goals

Proof state:
self : UnionFind
x : Fin self.size
⊢ parentD (self.findAux x).s (self.rootD ↑x) = self.rootD ↑x

Tactic:
rw [parentD_findAux]

Result:
self : UnionFind
x : Fin self.size
⊢ (if self.rootD ↑x = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s (self.rootD ↑x)) =
    self.rootD ↑x

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
h : ¬self.rootD ↑x = ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s (self.rootD ↑x) = self.rootD ↑x

Tactic:
rw [rootD_eq_self, parent, parentD_eq x.2] at h

Result:
case isFalse
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s (self.rootD ↑x) = self.rootD ↑x

Proof state:
self : UnionFind
x : Fin self.size
⊢ (if self.rootD ↑x = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s (self.rootD ↑x)) =
    self.rootD ↑x

Tactic:
split <;> [rfl; rename_i h]

Result:
case isFalse
self : UnionFind
x : Fin self.size
h : ¬self.rootD ↑x = ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s (self.rootD ↑x) = self.rootD ↑x

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s (self.rootD ↑x) = self.rootD ↑x

Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)

Result:
case isFalse
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s (self.rootD ↑x) = self.rootD ↑x

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s (self.rootD ↑x) = self.rootD ↑x

Tactic:
rw [← rootD_parent, parent, parentD_eq x.2]

Result:
case isFalse
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s (self.rootD self.arr[↑x].parent) = self.rootD self.arr[↑x].parent
-- Mathlib/Topology/Basic.lean
theorem nhds_basis_opens' (x : X) :
    (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 x ∧ IsOpen s) fun x => x

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsOpen s) fun x => x

Tactic:
convert nhds_basis_opens x using 2

Result:
case h.e'_4.h.a
X : Type u
inst✝ : TopologicalSpace X
x : X
x✝ : Set X
⊢ x✝ ∈ 𝓝 x ∧ IsOpen x✝ ↔ x ∈ x✝ ∧ IsOpen x✝

Proof state:
case h.e'_4.h.a
X : Type u
inst✝ : TopologicalSpace X
x : X
x✝ : Set X
⊢ x✝ ∈ 𝓝 x ∧ IsOpen x✝ ↔ x ∈ x✝ ∧ IsOpen x✝

Tactic:
exact and_congr_left_iff.2 IsOpen.mem_nhds_iff

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem lift_self (z : ℤ_[p]) : lift zmod_cast_comp_toZModPow z = z

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ∀ (n : ℕ), (toZModPow n).comp (RingHom.id ℤ_[p]) = toZModPow n

Tactic:
intro

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
n✝ : ℕ
⊢ (toZModPow n✝).comp (RingHom.id ℤ_[p]) = toZModPow n✝

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ (lift ⋯) z = (RingHom.id ℤ_[p]) z

Tactic:
rw [lift_unique zmod_cast_comp_toZModPow (RingHom.id ℤ_[p])]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ∀ (n : ℕ), (toZModPow n).comp (RingHom.id ℤ_[p]) = toZModPow n

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ (lift ⋯) z = z

Tactic:
show _ = RingHom.id _ z

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ (lift ⋯) z = (RingHom.id ℤ_[p]) z

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
n✝ : ℕ
⊢ (toZModPow n✝).comp (RingHom.id ℤ_[p]) = toZModPow n✝

Tactic:
rw [RingHom.comp_id]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Support.lean
theorem as_sum_support_C_mul_X_pow (p : R[X]) : p = ∑ i ∈ p.support, C (p.coeff i) * X ^ i :=
  _root_.trans p.as_sum_support <| by simp only [C_mul_X_pow_eq_monomial]

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ p.support, (monomial i) (p.coeff i) = ∑ i ∈ p.support, C (p.coeff i) * X ^ i

Tactic:
simp only [C_mul_X_pow_eq_monomial]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
/--
Two morphisms of sheaves of types `P ⟶ Q` coincide if the precompositions with morphisms
`yoneda.obj X ⟶ P` agree.
-/
lemma hom_ext_yoneda {P Q : Sheaf J (Type v)} {f g : P ⟶ Q}
    (h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), p ≫ f = p ≫ g) :
    f = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type v)
f g : P ⟶ Q
h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
ext X x

Result:
case h.w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type v)
f g : P ⟶ Q
h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.val.obj X
⊢ f.val.app X x = g.val.app X x

Proof state:
case h.w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type v)
f g : P ⟶ Q
h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.val.obj X
⊢ f.val.app X x = g.val.app X x

Tactic:
simpa only [yonedaEquiv_comp, Equiv.apply_symm_apply]
  using congr_arg (J.yonedaEquiv) (h _ (J.yonedaEquiv.symm x))

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_sub (f g : α →₁[μ] E) : integral (f - g) = integral f - integral g

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integral (f - g) = integral f - integral g

Tactic:
simp only [integral]

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integralCLM (f - g) = integralCLM f - integralCLM g

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integralCLM (f - g) = integralCLM f - integralCLM g

Tactic:
exact map_sub integralCLM f g

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem leftCosetEquivalence_equiv_fst (g : G) :
    LeftCosetEquivalence K g ((hSK.equiv g).fst : G)

Proof state:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
⊢ LeftCosetEquivalence (↑K) g (g * (↑(hSK.equiv g).2)⁻¹)

Tactic:
simp [LeftCosetEquivalence, leftCoset_eq_iff]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
⊢ LeftCosetEquivalence (↑K) g ↑(hSK.equiv g).1

Tactic:
rw [equiv_fst_eq_mul_inv]

Result:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
⊢ LeftCosetEquivalence (↑K) g (g * (↑(hSK.equiv g).2)⁻¹)
-- Mathlib/Data/Nat/Factorial/SuperFactorial.lean
theorem superFactorial_two_mul : ∀ n : ℕ,
    sf (2 * n) = (∏ i ∈ range n, (2 * i + 1) !) ^ 2 * 2 ^ n * n !
  | 0 => rfl
  | (n + 1) => by
    simp only [prod_range_succ, mul_pow, mul_add, mul_one, superFactorial_succ,
      superFactorial_two_mul n, factorial_succ]
    ring

Proof state:
n : ℕ
⊢ (2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!) *
      ((2 * n + 1) * (2 * n)! * ((∏ x ∈ range n, (2 * x + 1) * (2 * x)!) ^ 2 * 2 ^ n * n !)) =
    (∏ x ∈ range n, (2 * x + 1) * (2 * x)!) ^ 2 * ((2 * n + 1) ^ 2 * (2 * n)! ^ 2) * 2 ^ (n + 1) * ((n + 1) * n !)

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
⊢ sf 2 * (n + 1) = (∏ i ∈ range (n + 1), (2 * i + 1)!) ^ 2 * 2 ^ (n + 1) * (n + 1)!

Tactic:
simp only [prod_range_succ, mul_pow, mul_add, mul_one, superFactorial_succ,
  superFactorial_two_mul n, factorial_succ]

Result:
n : ℕ
⊢ (2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!) *
      ((2 * n + 1) * (2 * n)! * ((∏ x ∈ range n, (2 * x + 1) * (2 * x)!) ^ 2 * 2 ^ n * n !)) =
    (∏ x ∈ range n, (2 * x + 1) * (2 * x)!) ^ 2 * ((2 * n + 1) ^ 2 * (2 * n)! ^ 2) * 2 ^ (n + 1) * ((n + 1) * n !)
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.concat (h : a ∉ l) (h' : l.Nodup) : (l.concat a).Nodup

Proof state:
α : Type u
l : List α
a : α
h : a ∉ l
h' : l.Nodup
⊢ (l ++ [a]).Nodup

Tactic:
exact h'.append (nodup_singleton _) (disjoint_singleton.2 h)

Result:
no goals

Proof state:
α : Type u
l : List α
a : α
h : a ∉ l
h' : l.Nodup
⊢ (l.concat a).Nodup

Tactic:
rw [concat_eq_append]

Result:
α : Type u
l : List α
a : α
h : a ∉ l
h' : l.Nodup
⊢ (l ++ [a]).Nodup
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_mono_on_ae (hs : MeasurableSet s) (h : ∀ᵐ x ∂μ, x ∈ s → f x ≤ g x) :
    ∫ x in s, f x ∂μ ≤ ∫ x in s, g x ∂μ

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f g : X → ℝ
s : Set X
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ

Tactic:
refine setIntegral_mono_ae_restrict hf hg ?_

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f g : X → ℝ
s : Set X
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ f ≤ᶠ[ae (μ.restrict s)] g

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f g : X → ℝ
s : Set X
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ f ≤ᶠ[ae (μ.restrict s)] g

Tactic:
rwa [EventuallyLE, ae_restrict_iff' hs]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_cos : ∫ x in a..b, cos x = sin b - sin a

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, cos x = sin b - sin a

Tactic:
rw [integral_deriv_eq_sub']

Result:
case hderiv
a b : ℝ
⊢ deriv sin = cos

case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ sin x

case hcont
a b : ℝ
⊢ ContinuousOn cos [[a, b]]

Proof state:
case hderiv
a b : ℝ
⊢ deriv sin = cos

Tactic:
norm_num

Result:
no goals

Proof state:
case hcont
a b : ℝ
⊢ ContinuousOn cos [[a, b]]

Tactic:
exact continuousOn_cos

Result:
no goals

Proof state:
case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ sin x

Tactic:
simp only [differentiableAt_sin, implies_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  by
  rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat']

Proof state:
n : Nat
⊢ BitVec.ofNat 1 n = ofBool (decide (n % 2 = 1))

Tactic:
rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_append_of_pos {p : α → Bool} {l₁ l₂ : List α} (h : ∀ a ∈ l₁, p a) :
    (l₁ ++ l₂).takeWhile p = l₁ ++ l₂.takeWhile p

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : ∀ (a : α), a ∈ l₁ → p a = true
⊢ takeWhile p (l₁ ++ l₂) = l₁ ++ takeWhile p l₂

Tactic:
induction l₁ with
| nil => simp
| cons x xs ih => simp_all [takeWhile_cons]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
l₂ : List α
h : ∀ (a : α), a ∈ [] → p a = true
⊢ takeWhile p ([] ++ l₂) = [] ++ takeWhile p l₂

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : (∀ (a : α), a ∈ xs → p a = true) → takeWhile p (xs ++ l₂) = xs ++ takeWhile p l₂
h : ∀ (a : α), a ∈ x :: xs → p a = true
⊢ takeWhile p (x :: xs ++ l₂) = x :: xs ++ takeWhile p l₂

Tactic:
simp_all [takeWhile_cons]

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
lemma mem_closed_iff (s : Set M) :
    s ∈ (closure L).closed ↔ ∀ {n}, ∀ f : L.Functions n, ClosedUnder f s

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ s ∈ (closure L).closed ↔ ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s

Tactic:
refine ⟨fun h n f => ?_, fun h => ?_⟩

Result:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : s ∈ (closure L).closed
n : ℕ
f : L.Functions n
⊢ ClosedUnder f s

case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
⊢ s ∈ (closure L).closed

Proof state:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
h' : (closure L).toFun s = { carrier := s, fun_mem := ⋯ }
⊢ s ∈ (closure L).closed

Tactic:
exact congr_arg _ h'

Result:
no goals

Proof state:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : s ∈ (closure L).closed
n : ℕ
f : L.Functions n
⊢ ClosedUnder f s

Tactic:
rw [← h]

Result:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : s ∈ (closure L).closed
n : ℕ
f : L.Functions n
⊢ ClosedUnder f ↑((closure L).toFun s)

Proof state:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
⊢ s ∈ (closure L).closed

Tactic:
have h' : closure L s = ⟨s, h⟩ := closure_eq_of_le (refl _) subset_closure

Result:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
h' : (closure L).toFun s = { carrier := s, fun_mem := ⋯ }
⊢ s ∈ (closure L).closed

Proof state:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : s ∈ (closure L).closed
n : ℕ
f : L.Functions n
⊢ ClosedUnder f ↑((closure L).toFun s)

Tactic:
exact Substructure.fun_mem _ _

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem sumCasesOn {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ} (hf : Primrec f)
    (hg : Primrec₂ g) (hh : Primrec₂ h) : @Primrec _ σ _ _ fun a => Sum.casesOn (f a) (g a) (h a) :=
  option_some_iff.1 <|
    (cond (nat_bodd.comp <| encode_iff.2 hf)
          (option_map (Primrec.decode.comp <| nat_div2.comp <| encode_iff.2 hf) hh)
          (option_map (Primrec.decode.comp <| nat_div2.comp <| encode_iff.2 hf) hg)).of_eq
      fun a => by rcases f a with b | c <;> simp [Nat.div2_val, encodek]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
⊢ (bif (encode (f a)).bodd then Option.map (h a) (decode (encode (f a)).div2)
    else Option.map (g a) (decode (encode (f a)).div2)) =
    some (Sum.casesOn (f a) (g a) (h a))

Tactic:
rcases f a with b | c <;> simp [Nat.div2_val, encodek]

Result:
no goals