harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/NoncommProd.lean
@[to_additive]
lemma noncommProd_induction (s : Multiset α) (comm)
    (p : α → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p x) :
    p (s.noncommProd comm)

Proof state:
α : Type u_3
inst✝ : Monoid α
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p x
⊢ p (s.noncommProd comm)

Tactic:
induction' s using Quotient.inductionOn with l

Result:
case h
α : Type u_3
inst✝ : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
base : ∀ x ∈ ⟦l⟧, p x
⊢ p (noncommProd ⟦l⟧ comm)

Proof state:
case h
α : Type u_3
inst✝ : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
base : ∀ x ∈ l, p x
⊢ p l.prod

Tactic:
exact l.prod_induction p hom unit base

Result:
no goals

Proof state:
case h
α : Type u_3
inst✝ : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
base : ∀ x ∈ ⟦l⟧, p x
⊢ p (noncommProd ⟦l⟧ comm)

Tactic:
simp only [quot_mk_to_coe, noncommProd_coe, mem_coe] at base ⊢

Result:
case h
α : Type u_3
inst✝ : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
base : ∀ x ∈ l, p x
⊢ p l.prod
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : DHashMap α β)

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
a : α
c : Nat
⊢ ¬a ∈ empty c

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem cgf_zero' : cgf X μ 0 = log (μ Set.univ).toReal

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ cgf X μ 0 = log (μ Set.univ).toReal

Tactic:
simp only [cgf, mgf_zero']

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@[simp]
lemma nonsingular_zero : W'.Nonsingular 0 0 ↔ W'.a₆ = 0 ∧ (W'.a₃ ≠ 0 ∨ W'.a₄ ≠ 0)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ W'.Nonsingular 0 0 ↔ W'.a₆ = 0 ∧ (W'.a₃ ≠ 0 ∨ W'.a₄ ≠ 0)

Tactic:
rw [Nonsingular, equation_zero, evalEval_polynomialX_zero, neg_ne_zero, evalEval_polynomialY_zero,
  or_comm]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem treesOfNumNodesEq_card_eq_catalan (n : ℕ) : #(treesOfNumNodesEq n) = catalan n

Proof state:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ x ∈ antidiagonal n,
    ∀ y ∈ antidiagonal n,
      x ≠ y →
        Disjoint (pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2))
          (pairwiseNode (treesOfNumNodesEq y.1) (treesOfNumNodesEq y.2))

Tactic:
simp_rw [disjoint_left]

Result:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ x ∈ antidiagonal n,
    ∀ y ∈ antidiagonal n,
      x ≠ y →
        ∀ ⦃a : Tree Unit⦄,
          a ∈ pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2) →
            a ∉ pairwiseNode (treesOfNumNodesEq y.1) (treesOfNumNodesEq y.2)

Proof state:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ #(treesOfNumNodesEq (n + 1)) = catalan (n + 1)

Tactic:
rw [treesOfNumNodesEq_succ, card_biUnion, catalan_succ']

Result:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∑ u ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)) =
    ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ x ∈ antidiagonal n,
    ∀ y ∈ antidiagonal n,
      x ≠ y →
        Disjoint (pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2))
          (pairwiseNode (treesOfNumNodesEq y.1) (treesOfNumNodesEq y.2))

Proof state:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∑ u ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)) =
    ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

Tactic:
apply sum_congr rfl

Result:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ x ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2)) = catalan x.1 * catalan x.2

Proof state:
case hz

⊢ #(treesOfNumNodesEq 0) = catalan 0

Tactic:
simp

Result:
no goals

Proof state:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ x ∈ antidiagonal n,
    ∀ y ∈ antidiagonal n,
      x ≠ y →
        ∀ ⦃a : Tree Unit⦄,
          a ∈ pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2) →
            a ∉ pairwiseNode (treesOfNumNodesEq y.1) (treesOfNumNodesEq y.2)

Tactic:
aesop

Result:
no goals

Proof state:
case hi.mk
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
i j : ℕ
H : (i, j) ∈ antidiagonal n
⊢ #(pairwiseNode (treesOfNumNodesEq (i, j).1) (treesOfNumNodesEq (i, j).2)) = catalan (i, j).1 * catalan (i, j).2

Tactic:
rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]

Result:
no goals

Proof state:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ x ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2)) = catalan x.1 * catalan x.2

Tactic:
rintro ⟨i, j⟩ H

Result:
case hi.mk
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
i j : ℕ
H : (i, j) ∈ antidiagonal n
⊢ #(pairwiseNode (treesOfNumNodesEq (i, j).1) (treesOfNumNodesEq (i, j).2)) = catalan (i, j).1 * catalan (i, j).2
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem preservesMonomorphisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
    PreservesMonomorphisms G :=
  { preserves := fun {X} {Y} f hf =>
      ⟨by
        intro Z g h H
        replace H := congr_arg (adj.homEquiv Z Y).symm H
        rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
          Equiv.apply_eq_iff_eq] at H⟩ }

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
⊢ ∀ {Z : C} (g h : Z ⟶ G.obj X), g ≫ G.map f = h ≫ G.map f → g = h

Tactic:
intro Z g h H

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : g ≫ G.map f = h ≫ G.map f
⊢ g = h

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : g ≫ G.map f = h ≫ G.map f
⊢ g = h

Tactic:
replace H := congr_arg (adj.homEquiv Z Y).symm H

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : (adj.homEquiv Z Y).symm (g ≫ G.map f) = (adj.homEquiv Z Y).symm (h ≫ G.map f)
⊢ g = h

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : (adj.homEquiv Z Y).symm (g ≫ G.map f) = (adj.homEquiv Z Y).symm (h ≫ G.map f)
⊢ g = h

Tactic:
rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
  Equiv.apply_eq_iff_eq] at H

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem Composition.toCompositionAsSet_length (c : Composition n) :
    c.toCompositionAsSet.length = c.length

Proof state:
n : ℕ
c : Composition n
⊢ c.toCompositionAsSet.length = c.length

Tactic:
simp [Composition.toCompositionAsSet, CompositionAsSet.length, c.card_boundaries_eq_succ_length]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem inner_condExpL2_eq_inner_fun (hm : m ≤ m0) (f g : α →₂[μ] E)
    (hg : AEStronglyMeasurable[m] g μ) :
    ⟪(condExpL2 E 𝕜 hm f : α →₂[μ] E), g⟫₂ = ⟪f, g⟫₂

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑↑g) μ
⊢ inner (↑((condExpL2 E 𝕜 hm) f)) g = inner f g

Tactic:
symm

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑↑g) μ
⊢ inner f g = inner (↑((condExpL2 E 𝕜 hm) f)) g

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑↑g) μ
⊢ inner (f - ↑((orthogonalProjection (lpMeas E 𝕜 m 2 μ)) f)) g = 0

Tactic:
simp only [mem_lpMeas_iff_aeStronglyMeasurable.mpr hg, orthogonalProjection_inner_eq_zero f g]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑↑g) μ
⊢ inner f g = inner (↑((condExpL2 E 𝕜 hm) f)) g

Tactic:
rw [← sub_eq_zero, ← inner_sub_left, condExpL2]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑↑g) μ
⊢ inner (f - ↑((orthogonalProjection (lpMeas E 𝕜 m 2 μ)) f)) g = 0
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem mapEquiv_refl : mapEquiv AlgEquiv.refl = RingEquiv.refl (FractionalIdeal S P) :=
  RingEquiv.ext fun x => by simp

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
x : FractionalIdeal S P
⊢ (mapEquiv AlgEquiv.refl) x = (RingEquiv.refl (FractionalIdeal S P)) x

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_not_succ_of_ne_bsup {o : Ordinal.{u}} {f : ∀ a < o, Ordinal.{max u v}}
    (hf : ∀ {i : Ordinal} (h : i < o), f i h ≠ bsup.{_, v} o f) (a) :
    a < bsup.{_, v} o f → succ a < bsup.{_, v} o f

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f
a : Ordinal.{max u v}
⊢ a < o.bsup f → succ a < o.bsup f

Tactic:
rw [← sup_eq_bsup] at *

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ sup (o.familyOfBFamily f)
a : Ordinal.{max u v}
⊢ a < sup (o.familyOfBFamily f) → succ a < sup (o.familyOfBFamily f)

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ sup (o.familyOfBFamily f)
a : Ordinal.{max u v}
⊢ a < sup (o.familyOfBFamily f) → succ a < sup (o.familyOfBFamily f)

Tactic:
exact sup_not_succ_of_ne_sup fun i => hf _

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma CharP.neg_one_ne_one [Ring R] (p : ℕ) [CharP R p] [Fact (2 < p)] : (-1 : R) ≠ (1 : R)

Proof state:
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ -1 ≠ 1

Tactic:
rw [ne_comm, ← sub_ne_zero, sub_neg_eq_add, one_add_one_eq_two, ← Nat.cast_two, Ne,
  CharP.cast_eq_zero_iff R p 2]

Result:
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ ¬p ∣ 2

Proof state:
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ ¬p ∣ 2

Tactic:
exact fun h ↦ (Fact.out : 2 < p).not_le <| Nat.le_of_dvd Nat.zero_lt_two h

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem le_ndinter {s t u : Multiset α} : s ≤ ndinter t u ↔ s ≤ t ∧ s ⊆ u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u

Tactic:
simp [ndinter, le_filter, subset_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem det_fromBlocks_one₂₂ (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) :
    (Matrix.fromBlocks A B C 1).det = det (A - B * C)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible 1
⊢ (fromBlocks A B C 1).det = (A - B * C).det

Tactic:
rw [det_fromBlocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
⊢ (fromBlocks A B C 1).det = (A - B * C).det

Tactic:
haveI : Invertible (1 : Matrix n n α) := invertibleOne

Result:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible 1
⊢ (fromBlocks A B C 1).det = (A - B * C).det
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem range_map [DecidableEq γ] (g : β → γ) (f : α →ₛ β) : (f.map g).range = f.range.image g :=
  Finset.coe_injective <| by simp only [coe_range, coe_map, Finset.coe_image, range_comp]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : DecidableEq γ
g : β → γ
f : α →ₛ β
⊢ ↑(map g f).range = ↑(Finset.image g f.range)

Tactic:
simp only [coe_range, coe_map, Finset.coe_image, range_comp]

Result:
no goals
-- Mathlib/RingTheory/FinitePresentation.lean
theorem of_comp_finiteType (f : A →+* B) {g : B →+* C} (hg : (g.comp f).FinitePresentation)
    (hf : f.FiniteType) : g.FinitePresentation

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hg : (g.comp f).FinitePresentation
hf : f.FiniteType
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝¹ : Algebra.FinitePresentation A C
algebraizeInst✝ : Algebra.FiniteType A B
⊢ g.FinitePresentation

Tactic:
exact Algebra.FinitePresentation.of_restrict_scalars_finitePresentation A B C

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hg : (g.comp f).FinitePresentation
hf : f.FiniteType
⊢ g.FinitePresentation

Tactic:
algebraize [f, g, g.comp f]

Result:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hg : (g.comp f).FinitePresentation
hf : f.FiniteType
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝¹ : Algebra.FinitePresentation A C
algebraizeInst✝ : Algebra.FiniteType A B
⊢ g.FinitePresentation
-- Mathlib/Probability/Independence/Kernel.lean
theorem indepSet_empty_right {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ] (s : Set Ω) :
    IndepSet s ∅ κ μ

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s : Set Ω
⊢ IndepSet s ∅ κ μ

Tactic:
simp only [IndepSet, generateFrom_singleton_empty]

Result:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s : Set Ω
⊢ Indep (generateFrom {s}) ⊥ κ μ

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s : Set Ω
⊢ Indep (generateFrom {s}) ⊥ κ μ

Tactic:
exact indep_bot_right _

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[reassoc (attr := simp)]
lemma coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π (i : I) :
    (coyonedaOpColimitIsoLimitCoyoneda' F).inv ≫ coyoneda.map (colimit.ι F ⟨i⟩).op =
      limit.π (F.rightOp ⋙ coyoneda) i

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).inv ≫ coyoneda.map (colimit.ι F (op i)).op = limit.π (F.rightOp ⋙ coyoneda) i

Tactic:
rw [← coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, ← Category.assoc,
  Iso.inv_hom_id, Category.id_comp]

Result:
no goals
-- Mathlib/Order/Zorn.lean
theorem zorn_le₀ (s : Set α) (ih : ∀ c ⊆ s, IsChain (· ≤ ·) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) :
    ∃ m, Maximal (· ∈ s) m :=
  let ⟨⟨m, hms⟩, h⟩ :=
    @zorn_le s _ fun c hc =>
      let ⟨ub, hubs, hub⟩ :=
        ih (Subtype.val '' c) (fun _ ⟨⟨_, hx⟩, _, h⟩ => h ▸ hx)
          (by
            rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq
            exact hc hpc hqc fun t => hpq (Subtype.ext_iff.1 t))
      ⟨⟨ub, hubs⟩, fun ⟨_, _⟩ hc => hub _ ⟨_, hc, rfl⟩⟩
  ⟨m, hms, fun z hzs hmz => @h ⟨z, hzs⟩ hmz⟩

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
c : Set ↑s
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
p : { x // x ∈ s }
hpc : p ∈ c
q : { x // x ∈ s }
hqc : q ∈ c
hpq : ↑p ≠ ↑q
⊢ (fun x1 x2 => x1 ≤ x2) ↑p ↑q ∨ (fun x1 x2 => x1 ≤ x2) ↑q ↑p

Tactic:
exact hc hpc hqc fun t => hpq (Subtype.ext_iff.1 t)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
c : Set ↑s
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
⊢ IsChain (fun x1 x2 => x1 ≤ x2) (Subtype.val '' c)

Tactic:
rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
c : Set ↑s
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
p : { x // x ∈ s }
hpc : p ∈ c
q : { x // x ∈ s }
hqc : q ∈ c
hpq : ↑p ≠ ↑q
⊢ (fun x1 x2 => x1 ≤ x2) ↑p ↑q ∨ (fun x1 x2 => x1 ≤ x2) ↑q ↑p
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma ae_integrable_of_integrable_comp (h_int : Integrable f (κ ∘ₘ μ)) :
    ∀ᵐ x ∂μ, Integrable f (κ x)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
E : Type u_4
inst✝ : NormedAddCommGroup E
f : β → E
h_int :
  (∀ᵐ (y : α) ∂(Kernel.const Unit μ) (), Integrable f (κ y)) ∧
    Integrable (fun y => ∫ (z : β), ‖f z‖ ∂κ y) ((Kernel.const Unit μ) ())
⊢ ∀ᵐ (x : α) ∂μ, Integrable f (κ x)

Tactic:
exact h_int.1

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
E : Type u_4
inst✝ : NormedAddCommGroup E
f : β → E
h_int : Integrable f (⇑κ ∘ₘ μ)
⊢ ∀ᵐ (x : α) ∂μ, Integrable f (κ x)

Tactic:
rw [comp_eq_comp_const_apply, integrable_comp_iff h_int.1] at h_int

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
E : Type u_4
inst✝ : NormedAddCommGroup E
f : β → E
h_int :
  (∀ᵐ (y : α) ∂(Kernel.const Unit μ) (), Integrable f (κ y)) ∧
    Integrable (fun y => ∫ (z : β), ‖f z‖ ∂κ y) ((Kernel.const Unit μ) ())
⊢ ∀ᵐ (x : α) ∂μ, Integrable f (κ x)
-- Mathlib/Analysis/Analytic/Basic.lean
theorem hasFPowerSeriesAt_iff' :
    HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ z in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • p.coeff n) (f z)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))) ↔
    ∀ᶠ (a : 𝕜) in 𝓝 0, HasSum (fun n => (z₀ + a - z₀) ^ n • p.coeff n) (f (z₀ + a))

Tactic:
simp_rw [add_sub_cancel_left]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • p.coeff n) (f z)

Tactic:
rw [← map_add_left_nhds_zero, eventually_map, hasFPowerSeriesAt_iff]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))) ↔
    ∀ᶠ (a : 𝕜) in 𝓝 0, HasSum (fun n => (z₀ + a - z₀) ^ n • p.coeff n) (f (z₀ + a))
-- Mathlib/Data/Nat/Count.lean
theorem count_iff_forall {n : ℕ} : count p n = n ↔ ∀ n' < n, p n'

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = n ↔ ∀ n' < n, p n'

Tactic:
simpa [count_eq_card_filter_range, card_range, mem_range] using
  card_filter_eq_iff (p := p) (s := range n)

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem aeval_eq (h : IsAdjoinRoot S f) (p : R[X]) : aeval h.root p = h.map p :=
  Polynomial.induction_on p (fun x => by rw [aeval_C, h.algebraMap_apply])
    (fun p q ihp ihq => by rw [map_add, RingHom.map_add, ihp, ihq]) fun n x _ => by
    rw [map_mul, aeval_C, map_pow, aeval_X, RingHom.map_mul, ← h.algebraMap_apply,
      RingHom.map_pow, map_X]

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
p : R[X]
x : R
⊢ (aeval h.root) (C x) = h.map (C x)

Tactic:
rw [aeval_C, h.algebraMap_apply]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
p✝ p q : R[X]
ihp : (aeval h.root) p = h.map p
ihq : (aeval h.root) q = h.map q
⊢ (aeval h.root) (p + q) = h.map (p + q)

Tactic:
rw [map_add, RingHom.map_add, ihp, ihq]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
p : R[X]
n : ℕ
x : R
x✝ : (aeval h.root) (C x * X ^ n) = h.map (C x * X ^ n)
⊢ (aeval h.root) (C x * X ^ (n + 1)) = h.map (C x * X ^ (n + 1))

Tactic:
rw [map_mul, aeval_C, map_pow, aeval_X, RingHom.map_mul, ← h.algebraMap_apply,
  RingHom.map_pow, map_X]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
lemma IntegrableOn.of_finite [MeasurableSingletonClass α] {μ : Measure α} [IsFiniteMeasure μ]
    {s : Set α} (hs : s.Finite) {f : α → E} : IntegrableOn f s μ

Proof state:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
hs : s.Finite
f : α → E
⊢ IntegrableOn f s μ

Tactic:
simpa using IntegrableOn.finset (s := hs.toFinset)

Result:
no goals
-- Mathlib/Algebra/Algebra/RestrictScalars.lean
theorem RestrictScalars.addEquiv_symm_map_smul_smul (r : R) (s : S) (x : M) :
    (RestrictScalars.addEquiv R S M).symm ((r • s) • x) =
      r • (RestrictScalars.addEquiv R S M).symm (s • x)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ (addEquiv R S M).symm ((r • s) • x) = r • (addEquiv R S M).symm (s • x)

Tactic:
rw [Algebra.smul_def, mul_smul]

Result:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ (addEquiv R S M).symm ((algebraMap R S) r • s • x) = r • (addEquiv R S M).symm (s • x)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ (addEquiv R S M).symm ((algebraMap R S) r • s • x) = r • (addEquiv R S M).symm (s • x)

Tactic:
rfl

Result:
no goals