harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem repr_apply_apply (b : HilbertBasis ι 𝕜 E) (v : E) (i : ι) :
    b.repr v i = ⟪b i, v⟫

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
v : E
i : ι
⊢ ↑(b.repr v) i = inner (b i) v

Tactic:
classical
rw [← b.repr.inner_map_map (b i) v, b.repr_self, lp.inner_single_left]
simp

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
v : E
i : ι
⊢ ↑(b.repr v) i = inner 1 (↑(b.repr v) i)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
v : E
i : ι
⊢ ↑(b.repr v) i = inner (b i) v

Tactic:
rw [← b.repr.inner_map_map (b i) v, b.repr_self, lp.inner_single_left]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
v : E
i : ι
⊢ ↑(b.repr v) i = inner 1 (↑(b.repr v) i)
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem mem_matricesOver (I : Ideal R) (M : Matrix n n R) :
    M ∈ I.matricesOver n ↔ ∀ i j, M i j ∈ I

Proof state:
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
⊢ M ∈ matricesOver n I ↔ ∀ (i j : n), M i j ∈ I

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
@[simp] lemma coe_ne_zero (ψ : AddChar A M₀) : (ψ : A → M₀) ≠ 0 :=
  ne_iff.2 ⟨0, fun h ↦ by simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ⟩

Proof state:
A : Type u_1
M₀ : Type u_2
inst✝² : AddGroup A
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
ψ : AddChar A M₀
h : ψ 0 = 0 0
⊢ False

Tactic:
simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[nolint unusedHavesSuffices]
private lemma equivTree_right_inv : ∀ t, equivTreeToFun (equivTreeInvFun t) = t
  | Tree.nil => by simp [equivTreeInvFun, equivTreeToFun]
  | Tree.node _ _ _ => by simp [equivTreeInvFun, equivTreeToFun, equivTree_right_inv]

Proof state:
a✝² : Unit
a✝¹ a✝ : Tree Unit
⊢ DyckWord.equivTreeToFun (DyckWord.equivTreeInvFun (node a✝² a✝¹ a✝)) = node a✝² a✝¹ a✝

Tactic:
simp [equivTreeInvFun, equivTreeToFun, equivTree_right_inv]

Result:
no goals

Proof state:
⊢ DyckWord.equivTreeToFun (DyckWord.equivTreeInvFun Tree.nil) = Tree.nil

Tactic:
simp [equivTreeInvFun, equivTreeToFun]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasFDerivAt_inv' {x : R} (hx : x ≠ 0) :
    HasFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
R : Type u_5
inst✝¹ : NormedDivisionRing R
inst✝ : NormedAlgebra 𝕜 R
x : R
hx : x ≠ 0
⊢ HasFDerivAt Inv.inv (-((mulLeftRight 𝕜 R) x⁻¹) x⁻¹) x

Tactic:
simpa using hasFDerivAt_ring_inverse (Units.mk0 _ hx)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_sub_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n - y) n = Int.bmod (x - y) n

Proof state:
y x : Int
n : Nat
⊢ (x + -(↑n * (x / ↑n)) + -y).bmod n = (x + -y).bmod n

Tactic:
rw [←Int.mul_neg, Int.add_right_comm,  Int.bmod_add_mul_cancel]

Result:
no goals

Proof state:
y x : Int
n : Nat
⊢ (x % ↑n - y).bmod n = (x - y).bmod n

Tactic:
simp only [emod_def, Int.sub_eq_add_neg]

Result:
y x : Int
n : Nat
⊢ (x + -(↑n * (x / ↑n)) + -y).bmod n = (x + -y).bmod n
-- Mathlib/Algebra/Module/CharacterModule.lean
lemma eq_zero_of_character_apply {a : A} (h : ∀ c : CharacterModule A, c a = 0) : a = 0

Proof state:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : ∀ (c : CharacterModule A), c a = 0
⊢ a = 0

Tactic:
contrapose! h

Result:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : a ≠ 0
⊢ ∃ c, c a ≠ 0

Proof state:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : a ≠ 0
⊢ ∃ c, c a ≠ 0

Tactic:
exact exists_character_apply_ne_zero_of_ne_zero h

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_hom (s : Multiset α) {F : Type*} [FunLike F α β]
    [MonoidHomClass F α β] (f : F) :
    (s.map f).prod = f s.prod :=
  Quotient.inductionOn s fun l => by simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe]

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Multiset α
F : Type u_7
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
l : List α
⊢ (map ⇑f ⟦l⟧).prod = f (prod ⟦l⟧)

Tactic:
simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem piecewise_insert_of_ne {i j : α} (h : i ≠ j) [∀ i, Decidable (i ∈ insert j s)] :
    (insert j s).piecewise f g i = s.piecewise f g i

Proof state:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
i j : α
h : i ≠ j
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g i = s.piecewise f g i

Tactic:
simp [piecewise, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_one : (1#w).getMsbD i = (decide (i = w - 1) && decide (0 < w))

Proof state:
w i : Nat
⊢ (1#w).getMsbD i = (decide (i = w - 1) && decide (0 < w))

Tactic:
simp only [getMsbD]

Result:
w i : Nat
⊢ (decide (i < w) && (1#w).getLsbD (w - 1 - i)) = (decide (i = w - 1) && decide (0 < w))

Proof state:
w i : Nat
⊢ (decide (i < w) && (1#w).getLsbD (w - 1 - i)) = (decide (i = w - 1) && decide (0 < w))

Tactic:
by_cases h : 0 < w <;> by_cases h' : i = w - 1 <;> simp [h, h'] <;> omega

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coverage.lean
theorem isSheaf_iff_isLimit_coverage (K : Coverage C) (P : Cᵒᵖ ⥤ D) :
    Presheaf.IsSheaf (toGrothendieck _ K) P ↔ ∀ ⦃X : C⦄ (R : Presieve X),
      R ∈ K.covering X →
        Nonempty (IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op))

Proof state:
C : Type u_1
D : Type u_4
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Category.{u_3, u_4} D
K : Coverage C
P : Cᵒᵖ ⥤ D
⊢ IsSheaf (toGrothendieck C K) P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.covering X, Nonempty (IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op))

Tactic:
simp only [Presheaf.IsSheaf, Presieve.isSheaf_coverage, isLimit_iff_isSheafFor,
  ← Presieve.isSheafFor_iff_generate]

Result:
C : Type u_1
D : Type u_4
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Category.{u_3, u_4} D
K : Coverage C
P : Cᵒᵖ ⥤ D
⊢ (∀ (E : D) {X : C}, ∀ R ∈ K.covering X, Presieve.IsSheafFor (P ⋙ coyoneda.obj (Opposite.op E)) R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.covering X, ∀ (E : Dᵒᵖ), Presieve.IsSheafFor (P ⋙ coyoneda.obj E) R

Proof state:
C : Type u_1
D : Type u_4
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Category.{u_3, u_4} D
K : Coverage C
P : Cᵒᵖ ⥤ D
⊢ (∀ (E : D) {X : C}, ∀ R ∈ K.covering X, Presieve.IsSheafFor (P ⋙ coyoneda.obj (Opposite.op E)) R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.covering X, ∀ (E : Dᵒᵖ), Presieve.IsSheafFor (P ⋙ coyoneda.obj E) R

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem cantorFunctionAux_zero (f : ℕ → Bool) : cantorFunctionAux c f 0 = cond (f 0) 1 0

Proof state:
c : ℝ
f : ℕ → Bool
⊢ cantorFunctionAux c f 0 = bif f 0 then 1 else 0

Tactic:
cases h : f 0 <;> simp [h]

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem card_sigmaLift :
    (sigmaLift f a b).card = dite (a.1 = b.1) (fun h => (f (h ▸ a.2) b.2).card) fun _ => 0

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ #(if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) =
    if h : a.fst = b.fst then #(f (h ▸ a.snd) b.snd) else 0

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

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ #(sigmaLift f a b) = if h : a.fst = b.fst then #(f (h ▸ a.snd) b.snd) else 0

Tactic:
simp_rw [sigmaLift]

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ #(if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) =
    if h : a.fst = b.fst then #(f (h ▸ a.snd) b.snd) else 0
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma castAdd_inj {a b : Fin m} : castAdd n a = castAdd n b ↔ a = b

Proof state:
n m : ℕ
a b : Fin m
⊢ castAdd n a = castAdd n b ↔ a = b

Tactic:
simp [Fin.ext_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Integral.lean
theorem integrable_comp_div_left (f : G → F) [IsInvInvariant μ] [IsMulLeftInvariant μ] (g : G) :
    Integrable (fun t => f (g / t)) μ ↔ Integrable f μ

Proof state:
case h.e'_6.h.h.e'_1
G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
h : Integrable (fun t => f (g / t)) μ
x✝ : G
⊢ x✝ = g / (g⁻¹ * x✝)⁻¹

Tactic:
simp_rw [div_inv_eq_mul, mul_inv_cancel_left]

Result:
no goals

Proof state:
G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
h : Integrable (fun t => f (g / t)) μ
⊢ Integrable f μ

Tactic:
convert h.comp_inv.comp_mul_left g⁻¹

Result:
case h.e'_6.h.h.e'_1
G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
h : Integrable (fun t => f (g / t)) μ
x✝ : G
⊢ x✝ = g / (g⁻¹ * x✝)⁻¹

Proof state:
G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ Integrable (fun t => f (g / t)) μ ↔ Integrable f μ

Tactic:
refine ⟨fun h => ?_, fun h => h.comp_div_left g⟩

Result:
G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
h : Integrable (fun t => f (g / t)) μ
⊢ Integrable f μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_replicate_nil : (replicate n ([] : List α)).flatten = []

Proof state:
n : Nat
α : Type u_1
⊢ (replicate n []).flatten = []

Tactic:
induction n <;> simp_all [replicate_succ]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos {x y : ℝ*} :
    InfiniteNeg x → ¬Infinitesimal y → 0 < y → InfiniteNeg (x * y)

Proof state:
x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg

Tactic:
rw [← infinitePos_neg, ← infinitePos_neg, neg_mul_eq_neg_mul]

Result:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (-x * y).InfinitePos

Proof state:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (-x * y).InfinitePos

Tactic:
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_modifyKey [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β))
    (hl : DistinctKeys l) :
    getValue? k' (modifyKey k f l)  =
      if k == k' then
        (getValue? k l).map f
      else
        getValue? k' l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getValue? k' (modifyKey k f l) = if (k == k') = true then Option.map f (getValue? k l) else getValue? k' l

Tactic:
simp [modifyKey_eq_alterKey, getValue?_alterKey, hl]

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_cons (s : Finset α) (a : α) (f : α → β)
    (ha : a ∉ s) (comm) :
    noncommProd (cons a s ha) f comm =
      f a * noncommProd s f (comm.mono fun _ => Finset.mem_cons.2 ∘ .inr)

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯

Tactic:
simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons]

Result:
no goals
-- Mathlib/Data/Analysis/Topology.lean
theorem mem_nhds [T : TopologicalSpace α] (F : Realizer α) {s : Set α} {a : α} :
    s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F b ∧ F.F b ⊆ s

Proof state:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
have := @mem_nhds_toTopsp _ _ F.F s a

Result:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s

Proof state:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
rwa [F.eq] at this

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem induced_sInf {s : Set (TopologicalSpace α)} :
    TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)

Proof state:
α : Type u_1
β : Type u_2
g : β → α
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)

Tactic:
rw [sInf_eq_iInf', sInf_image', induced_iInf]

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem coe_natLERec (m n : ℕ) (h : m ≤ n) :
    (natLERec f' m n h : G' m → G' n) = Nat.leRecOn h (@fun k => f' k)

Proof state:
case intro.h.succ
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih : ∀ (h : m ≤ m + k), (natLERec f' m (m + k) h) x = Nat.leRecOn h (fun k => ⇑(f' k)) x
h : m ≤ m + (k + 1)
⊢ (natLERec f' m (m + (k + 1)) h) x = Nat.leRecOn h (fun k => ⇑(f' k)) x

Tactic:
erw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
  Embedding.comp_apply, ih]

Result:
no goals

Proof state:
case intro.h
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
x : G' m
⊢ (natLERec f' m (m + k) h) x = Nat.leRecOn h (fun k => ⇑(f' k)) x

Tactic:
induction' k with k ih

Result:
case intro.h.zero
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
h : m ≤ m + 0
⊢ (natLERec f' m (m + 0) h) x = Nat.leRecOn h (fun k => ⇑(f' k)) x

case intro.h.succ
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih : ∀ (h : m ≤ m + k), (natLERec f' m (m + k) h) x = Nat.leRecOn h (fun k => ⇑(f' k)) x
h : m ≤ m + (k + 1)
⊢ (natLERec f' m (m + (k + 1)) h) x = Nat.leRecOn h (fun k => ⇑(f' k)) x

Proof state:
case intro.h.zero
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
h : m ≤ m + 0
⊢ (natLERec f' m (m + 0) h) x = Nat.leRecOn h (fun k => ⇑(f' k)) x

Tactic:
erw [natLERec, Nat.leRecOn_self, Embedding.refl_apply, Nat.leRecOn_self]

Result:
no goals

Proof state:
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m n : ℕ
h : m ≤ n
⊢ ⇑(natLERec f' m n h) = fun a => Nat.leRecOn h (fun k => ⇑(f' k)) a

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h

Result:
case intro
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
⊢ ⇑(natLERec f' m (m + k) h) = fun a => Nat.leRecOn h (fun k => ⇑(f' k)) a

Proof state:
case intro
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
⊢ ⇑(natLERec f' m (m + k) h) = fun a => Nat.leRecOn h (fun k => ⇑(f' k)) a

Tactic:
ext x

Result:
case intro.h
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
x : G' m
⊢ (natLERec f' m (m + k) h) x = Nat.leRecOn h (fun k => ⇑(f' k)) x
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem diagonalObjPullbackFstIso_hom_fst_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (diagonalObjPullbackFstIso f g).hom ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
      pullback.snd _ _ ≫ pullback.snd _ _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).hom ≫
      fst (snd g g ≫ g) f ≫ snd g g =
    snd (fst f g) (fst f g) ≫ snd f g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).hom ≫ fst (snd g g ≫ g) f ≫ snd g g = snd (fst f g) (fst f g) ≫ snd f g

Tactic:
delta diagonalObjPullbackFstIso

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).hom ≫
      fst (snd g g ≫ g) f ≫ snd g g =
    snd (fst f g) (fst f g) ≫ snd f g
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem _root_.MeasurableEmbedding.setIntegral_map {Y} {_ : MeasurableSpace Y} {f : X → Y}
    (hf : MeasurableEmbedding f) (g : Y → E) (s : Set Y) :
    ∫ y in s, g y ∂Measure.map f μ = ∫ x in f ⁻¹' s, g (f x) ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
x✝ : MeasurableSpace Y
f : X → Y
hf : MeasurableEmbedding f
g : Y → E
s : Set Y
⊢ ∫ (y : Y) in s, g y ∂Measure.map f μ = ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ

Tactic:
rw [hf.restrict_map, hf.integral_map]

Result:
no goals
-- Mathlib/Algebra/Lie/TraceForm.lean
/-- Given a representation `M` of a Lie algebra `L`, the action of any `x : L` is skew-adjoint wrt
the trace form. -/
lemma traceForm_apply_lie_apply' (x y z : L) :
    traceForm R L M ⁅x, y⁆ z = - traceForm R L M y ⁅x, z⁆ :=
  calc traceForm R L M ⁅x, y⁆ z
      = - traceForm R L M ⁅y, x⁆ z

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y z : L
⊢ ((traceForm R L M) ⁅x, y⁆) z = -((traceForm R L M) ⁅y, x⁆) z

Tactic:
rw [← lie_skew x y, map_neg, LinearMap.neg_apply]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y z : L
⊢ -((traceForm R L M) ⁅y, x⁆) z = -((traceForm R L M) y) ⁅x, z⁆

Tactic:
rw [traceForm_apply_lie_apply]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
lemma shrink [UnivLE.{w, w'}] :
    IsStableUnderTransfiniteComposition.{w} W where
  isStableUnderTransfiniteCompositionOfShape J _ _ _ _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
inst✝¹ : W.IsStableUnderTransfiniteComposition
inst✝ : UnivLE.{w, w'}
J : Type w
x✝³ : LinearOrder J
x✝² : SuccOrder J
x✝¹ : OrderBot J
x✝ : WellFoundedLT J
⊢ W.IsStableUnderTransfiniteCompositionOfShape J

Tactic:
rw [isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso W
  (orderIsoShrink.{w'} J)]

Result:
C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
inst✝¹ : W.IsStableUnderTransfiniteComposition
inst✝ : UnivLE.{w, w'}
J : Type w
x✝³ : LinearOrder J
x✝² : SuccOrder J
x✝¹ : OrderBot J
x✝ : WellFoundedLT J
⊢ W.IsStableUnderTransfiniteCompositionOfShape (Shrink.{w', w} J)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
inst✝¹ : W.IsStableUnderTransfiniteComposition
inst✝ : UnivLE.{w, w'}
J : Type w
x✝³ : LinearOrder J
x✝² : SuccOrder J
x✝¹ : OrderBot J
x✝ : WellFoundedLT J
⊢ W.IsStableUnderTransfiniteCompositionOfShape (Shrink.{w', w} J)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem vector_cons {n} : Primrec₂ (@List.Vector.cons α n) :=
  vector_toList_iff.1 <| by simpa using list_cons.comp fst (vector_toList_iff.2 snd)

Proof state:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ Primrec fun a => (a.1 ::ᵥ a.2).toList

Tactic:
simpa using list_cons.comp fst (vector_toList_iff.2 snd)

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean
lemma finsetSum_mem {ι : Type*} (s : Finset ι) (f : ι → R) (hs : ∀ x ∈ s, f x ∈ I) :
    s.sum f ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (s.sum f) (∑ _x ∈ ?m.1847, 0)

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.1844

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Finset ?m.1845

Tactic:
exact I.ringCon.finsetSum s hs

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ s.sum f ∈ I

Tactic:
rw [mem_iff, ← Finset.sum_const_zero]

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (s.sum f) (∑ _x ∈ ?m.1847, 0)

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.1844

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Finset ?m.1845
-- Mathlib/FieldTheory/Separable.lean
theorem Separable.isCoprime {f g : R[X]} (h : (f * g).Separable) : IsCoprime f g

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ IsCoprime f g

Tactic:
have := h.of_mul_left_left

Result:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative (f * g))
⊢ IsCoprime f g

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative f * g + f * derivative g)
⊢ IsCoprime f g

Tactic:
exact IsCoprime.of_mul_right_right (IsCoprime.of_add_mul_left_right this)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative (f * g))
⊢ IsCoprime f g

Tactic:
rw [derivative_mul] at this

Result:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative f * g + f * derivative g)
⊢ IsCoprime f g