harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem mem_ker_toPermHom_iff :
    k ∈ (toPermHom g).ker ↔ ∀ c ∈ g.cycleFactorsFinset, Commute (k : Perm α) c

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
⊢ k ∈ (toPermHom g).ker ↔ ∀ c ∈ g.cycleFactorsFinset, Commute (↑k) c

Tactic:
simp only [toPermHom, MonoidHom.mem_ker, DFunLike.ext_iff, Subtype.forall]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
⊢ (∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
      ((MulAction.toPermHom ↥(centralizer {g}) { x // x ∈ g.cycleFactorsFinset }) k) ⟨a, b⟩ = 1 ⟨a, b⟩) ↔
    ∀ c ∈ g.cycleFactorsFinset, Commute (↑k) c

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
x✝¹ : Perm α
x✝ : x✝¹ ∈ g.cycleFactorsFinset
⊢ ((MulAction.toPermHom ↥(centralizer {g}) { x // x ∈ g.cycleFactorsFinset }) k) ⟨x✝¹, x✝⟩ = 1 ⟨x✝¹, x✝⟩ ↔
    Commute (↑k) x✝¹

Tactic:
simp [← Subtype.coe_inj, commute_iff_eq, mul_inv_eq_iff_eq_mul]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
⊢ (∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset),
      ((MulAction.toPermHom ↥(centralizer {g}) { x // x ∈ g.cycleFactorsFinset }) k) ⟨a, b⟩ = 1 ⟨a, b⟩) ↔
    ∀ c ∈ g.cycleFactorsFinset, Commute (↑k) c

Tactic:
refine forall₂_congr (fun _ _ ↦ ?_)

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
x✝¹ : Perm α
x✝ : x✝¹ ∈ g.cycleFactorsFinset
⊢ ((MulAction.toPermHom ↥(centralizer {g}) { x // x ∈ g.cycleFactorsFinset }) k) ⟨x✝¹, x✝⟩ = 1 ⟨x✝¹, x✝⟩ ↔
    Commute (↑k) x✝¹
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_multiset_map_count [DecidableEq α] (s : Multiset α) {M : Type*} [CommMonoid M]
    (f : α → M) : (s.map f).prod = ∏ m ∈ s.toFinset, f m ^ s.count m

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
s : Multiset α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
⊢ (Multiset.map f s).prod = ∏ m ∈ s.toFinset, f m ^ Multiset.count m s

Tactic:
refine Quot.induction_on s fun l => ?_

Result:
α : Type u_3
inst✝¹ : DecidableEq α
s : Multiset α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
l : List α
⊢ (Multiset.map f (Quot.mk (⇑(isSetoid α)) l)).prod =
    ∏ m ∈ Multiset.toFinset (Quot.mk (⇑(isSetoid α)) l), f m ^ Multiset.count m (Quot.mk (⇑(isSetoid α)) l)

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
s : Multiset α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
l : List α
⊢ (Multiset.map f (Quot.mk (⇑(isSetoid α)) l)).prod =
    ∏ m ∈ Multiset.toFinset (Quot.mk (⇑(isSetoid α)) l), f m ^ Multiset.count m (Quot.mk (⇑(isSetoid α)) l)

Tactic:
simp [prod_list_map_count l f]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
lemma supDegree_toLex_C (r : R) : supDegree toLex (C (σ := σ) r) = 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
r : R
⊢ supDegree (⇑toLex) (C r) = 0

Tactic:
exact (supDegree_single _ r).trans (ite_eq_iff'.mpr ⟨fun _ => rfl, fun _ => rfl⟩)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
r : R
⊢ supDegree (⇑toLex) (C r) = 0

Tactic:
classical
  exact (supDegree_single _ r).trans (ite_eq_iff'.mpr ⟨fun _ => rfl, fun _ => rfl⟩)

Result:
no goals
-- Mathlib/Order/Filter/Ker.lean
@[simp] lemma ker_comap (m : α → β) (f : Filter β) : ker (comap m f) = m ⁻¹' ker f

Proof state:
case h
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
⊢ (∀ y ∈ f, ∀ (x : Set α), m ⁻¹' y ⊆ x → a ∈ x) ↔ ∀ s ∈ f, m a ∈ s

Tactic:
exact forall₂_congr fun s _ ↦ ⟨fun h ↦ h _ Subset.rfl, fun ha t ht ↦ ht ha⟩

Result:
no goals

Proof state:
case h
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
⊢ a ∈ (comap m f).ker ↔ a ∈ m ⁻¹' f.ker

Tactic:
simp only [mem_ker, mem_comap, forall_exists_index, and_imp, @forall_swap (Set α), mem_preimage]

Result:
case h
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
⊢ (∀ y ∈ f, ∀ (x : Set α), m ⁻¹' y ⊆ x → a ∈ x) ↔ ∀ s ∈ f, m a ∈ s

Proof state:
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
⊢ (comap m f).ker = m ⁻¹' f.ker

Tactic:
ext a

Result:
case h
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
⊢ a ∈ (comap m f).ker ↔ a ∈ m ⁻¹' f.ker
-- Mathlib/Data/ZMod/Basic.lean
theorem mul_inv_eq_gcd {n : ℕ} (a : ZMod n) : a * a⁻¹ = Nat.gcd a.val n

Proof state:
n : ℕ
a : ZMod n
⊢ a * a⁻¹ = ↑(a.val.gcd n)

Tactic:
rcases n with - | n

Result:
case zero
a : ZMod 0
⊢ a * a⁻¹ = ↑(a.val.gcd 0)

case succ
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = ↑(a.val.gcd (n + 1))

Proof state:
case succ
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = ↑(a.val.gcd (n + 1))

Tactic:
calc
  a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
    rw [natCast_self, zero_mul, add_zero]
  _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
    push_cast
    rw [natCast_zmod_val]
    rfl
  _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl

Result:
no goals

Proof state:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + (↑n + 1) * ↑(a.val.gcdB n.succ) = ↑a.val * ↑(a.val.gcdA n.succ) + (↑n + 1) * ↑(a.val.gcdB n.succ)

Tactic:
rw [natCast_zmod_val]

Result:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + (↑n + 1) * ↑(a.val.gcdB n.succ) = a * ↑(a.val.gcdA n.succ) + (↑n + 1) * ↑(a.val.gcdB n.succ)

Proof state:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + ↑n.succ * ↑(a.val.gcdB n.succ) = ↑(↑a.val * a.val.gcdA n.succ + ↑n.succ * a.val.gcdB n.succ)

Tactic:
push_cast

Result:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + (↑n + 1) * ↑(a.val.gcdB n.succ) = ↑a.val * ↑(a.val.gcdA n.succ) + (↑n + 1) * ↑(a.val.gcdB n.succ)

Proof state:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = a * a⁻¹ + ↑n.succ * ↑(a.val.gcdB n.succ)

Tactic:
rw [natCast_self, zero_mul, add_zero]

Result:
no goals

Proof state:
a : ℤ
⊢ a * a.sign = ↑a.natAbs

Tactic:
rw [Int.mul_sign]

Result:
no goals

Proof state:
n : ℕ
a : ZMod (n + 1)
⊢ ↑↑(a.val.gcd n.succ) = ↑(a.val.gcd n.succ)

Tactic:
rfl

Result:
no goals

Proof state:
case zero
a : ZMod 0
⊢ a * a⁻¹ = ↑(a.val.gcd 0)

Tactic:
dsimp [ZMod] at a ⊢

Result:
case zero
a : ℤ
⊢ a * a⁻¹ = ↑((val a).gcd 0)

Proof state:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + (↑n + 1) * ↑(a.val.gcdB n.succ) = a * ↑(a.val.gcdA n.succ) + (↑n + 1) * ↑(a.val.gcdB n.succ)

Tactic:
rfl

Result:
no goals

Proof state:
a : ℤ
⊢ ↑a.natAbs = ↑(a.natAbs.gcd 0)

Tactic:
rw [Nat.gcd_zero_right]

Result:
no goals

Proof state:
case zero
a : ℤ
⊢ a * a⁻¹ = ↑((val a).gcd 0)

Tactic:
calc
  _ = a * Int.sign a := rfl
  _ = a.natAbs := by rw [Int.mul_sign]
  _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]

Result:
no goals

Proof state:
n : ℕ
a : ZMod (n + 1)
⊢ ↑(↑a.val * a.val.gcdA n.succ + ↑n.succ * a.val.gcdB n.succ) = ↑(a.val.gcd n.succ)

Tactic:
rw [← Nat.gcd_eq_gcd_ab a.val n.succ]

Result:
n : ℕ
a : ZMod (n + 1)
⊢ ↑↑(a.val.gcd n.succ) = ↑(a.val.gcd n.succ)
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
@[simp]
protected lemma disjoint_mk_iff {p q : Submodule R M}
    (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) :
    Disjoint (α := f.invtSubmodule) ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint p q

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint p q

Tactic:
rw [disjoint_iff, disjoint_iff, Sublattice.mk_inf_mk,
  Subtype.mk_eq_bot_iff (⊥ : f.invtSubmodule).property]

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem of_ufd_of_unique_irreducible {R : Type u} [CommRing R] [IsDomain R]
    [UniqueFactorizationMonoid R] (h₁ : ∃ p : R, Irreducible p)
    (h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q) :
    IsDiscreteValuationRing R

Proof state:
case intro.refine_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = span {p}

Tactic:
intro I

Result:
case intro.refine_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
⊢ (fun P => P ≠ ⊥ ∧ P.IsPrime) I → I = span {p}

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : Submodule.span R {Submodule.IsPrincipal.generator I} ≠ ⊥
hI : IsPrime (Submodule.span R {Submodule.IsPrincipal.generator I})
⊢ Irreducible (Submodule.IsPrincipal.generator I)

Tactic:
erw [Ne, span_singleton_eq_bot] at I0

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : ¬Submodule.IsPrincipal.generator I = 0
hI : IsPrime (Submodule.span R {Submodule.IsPrincipal.generator I})
⊢ Irreducible (Submodule.IsPrincipal.generator I)

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Tactic:
obtain ⟨p, hp⟩ := h₁

Result:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime
-- Mathlib/NumberTheory/LSeries/Convolution.lean
/-- We give an expression of the `LSeries.term` of the convolution of two functions
in terms of a sum over `Nat.divisorsAntidiagonal`. -/
lemma term_convolution (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) :
    term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Proof state:
case inl
f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s 0 = ∑ p ∈ divisorsAntidiagonal 0, term f s p.1 * term g s p.2

Tactic:
simp

Result:
no goals

Proof state:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ f p.1 * g p.2 / ↑n ^ s = term f s p.1 * term g s p.2

Tactic:
have ⟨hp₁, hp₂⟩ := ne_zero_of_mem_divisorsAntidiagonal hp

Result:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / ↑n ^ s = term f s p.1 * term g s p.2

Proof state:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Tactic:
rw [term_of_ne_zero hn, convolution_def, Finset.sum_div]

Result:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisorsAntidiagonal, f i.1 * g i.2 / ↑n ^ s = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Proof state:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / ↑n ^ s = term f s p.1 * term g s p.2

Tactic:
rw [term_of_ne_zero hp₁, term_of_ne_zero hp₂, mul_comm_div, div_div, ← mul_div_assoc,
  ← natCast_mul_natCast_cpow, ← cast_mul, mul_comm p.2, (mem_divisorsAntidiagonal.mp hp).1]

Result:
no goals

Proof state:
f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s 0 = ∑ p ∈ divisorsAntidiagonal 0, term f s p.1 * term g s p.2

case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Proof state:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisorsAntidiagonal, f i.1 * g i.2 / ↑n ^ s = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Tactic:
refine Finset.sum_congr rfl fun p hp ↦ ?_

Result:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ f p.1 * g p.2 / ↑n ^ s = term f s p.1 * term g s p.2
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem withBotCoe_subset_iff {I J : WithBot (Box ι)} : (I : Set (ι → ℝ)) ⊆ J ↔ I ≤ J

Proof state:
case bot
ι : Type u_1
J : WithBot (Box ι)
⊢ ↑⊥ ⊆ ↑J ↔ ⊥ ≤ J

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
I J : WithBot (Box ι)
⊢ ↑I ⊆ ↑J ↔ I ≤ J

Tactic:
induction I

Result:
case bot
ι : Type u_1
J : WithBot (Box ι)
⊢ ↑⊥ ⊆ ↑J ↔ ⊥ ≤ J

case coe
ι : Type u_1
J : WithBot (Box ι)
a✝ : Box ι
⊢ ↑↑a✝ ⊆ ↑J ↔ ↑a✝ ≤ J

Proof state:
case coe.bot
ι : Type u_1
a✝ : Box ι
⊢ ↑↑a✝ ⊆ ↑⊥ ↔ ↑a✝ ≤ ⊥

Tactic:
simp [subset_empty_iff]

Result:
no goals

Proof state:
case coe
ι : Type u_1
J : WithBot (Box ι)
a✝ : Box ι
⊢ ↑↑a✝ ⊆ ↑J ↔ ↑a✝ ≤ J

Tactic:
induction J

Result:
case coe.bot
ι : Type u_1
a✝ : Box ι
⊢ ↑↑a✝ ⊆ ↑⊥ ↔ ↑a✝ ≤ ⊥

case coe.coe
ι : Type u_1
a✝¹ a✝ : Box ι
⊢ ↑↑a✝¹ ⊆ ↑↑a✝ ↔ ↑a✝¹ ≤ ↑a✝

Proof state:
case coe.coe
ι : Type u_1
a✝¹ a✝ : Box ι
⊢ ↑↑a✝¹ ⊆ ↑↑a✝ ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem closure_openSegment (x y : E) : closure (openSegment 𝕜 x y) = [x -[𝕜] y]

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝¹¹ : LinearOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ closure (openSegment 𝕜 x y) = [x-[𝕜]y]

Tactic:
rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]

Result:
𝕜 : Type u_2
E : Type u_3
inst✝¹¹ : LinearOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ closure ((fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1) = (fun θ => (1 - θ) • x + θ • y) '' closure (Ioo 0 1)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝¹¹ : LinearOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ => (1 - θ) • x + θ • y

Tactic:
fun_prop

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝¹¹ : LinearOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ closure ((fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1) = (fun θ => (1 - θ) • x + θ • y) '' closure (Ioo 0 1)

Tactic:
exact (image_closure_of_isCompact (isBounded_Ioo _ _).isCompact_closure <|
  Continuous.continuousOn <| by fun_prop).symm

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_mono_on_of_le_Ioo [NoAtoms μ] (h : ∀ x ∈ Ioo a b, f x ≤ g x) :
    (∫ u in a..b, f u ∂μ) ≤ ∫ u in a..b, g u ∂μ

Proof state:
case h
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∀ x ∈ Ioo a b, f x ≤ g x

Tactic:
exact h

Result:
no goals

Proof state:
case hg
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn g (Ioo a b) μ

Tactic:
apply hg.1.mono Ioo_subset_Ioc_self le_rfl

Result:
no goals

Proof state:
case hs
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ MeasurableSet (Ioo a b)

Tactic:
exact measurableSet_Ioo

Result:
no goals

Proof state:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

Tactic:
simp only [integral_of_le hab, integral_Ioc_eq_integral_Ioo]

Result:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∫ (u : ℝ) in Ioo a b, f u ∂μ ≤ ∫ (u : ℝ) in Ioo a b, g u ∂μ

Proof state:
case hf
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn f (Ioo a b) μ

Tactic:
apply hf.1.mono Ioo_subset_Ioc_self le_rfl

Result:
no goals

Proof state:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∫ (u : ℝ) in Ioo a b, f u ∂μ ≤ ∫ (u : ℝ) in Ioo a b, g u ∂μ

Tactic:
apply setIntegral_mono_on

Result:
case hf
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn f (Ioo a b) μ

case hg
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn g (Ioo a b) μ

case hs
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ MeasurableSet (Ioo a b)

case h
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∀ x ∈ Ioo a b, f x ≤ g x
-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
@[reassoc (attr := simp)]
lemma functorEnriched_comp_id [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₂] :
    (ρ_ (functorEnrichedHom V F₁ F₂)).inv ≫
      functorEnrichedHom V F₁ F₂ ◁ functorEnrichedId V F₂ ≫
        functorEnrichedComp V F₁ F₂ F₂ = 𝟙 (functorEnrichedHom V F₁ F₂)

Proof state:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasFunctorEnrichedHom V F₂ F₂
⊢ (ρ_ (functorEnrichedHom V F₁ F₂)).inv ≫
      functorEnrichedHom V F₁ F₂ ◁ functorEnrichedId V F₂ ≫ functorEnrichedComp V F₁ F₂ F₂ =
    𝟙 (functorEnrichedHom V F₁ F₂)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma indicator_one_inj (h : indicator s (1 : ι → M₀) = indicator t 1) : s = t

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
⊢ s = t

Tactic:
ext

Result:
case h
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
x✝ : ι
⊢ x✝ ∈ s ↔ x✝ ∈ t

Proof state:
case h
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
x✝ : ι
⊢ x✝ ∈ s ↔ x✝ ∈ t

Tactic:
simp_rw [← indicator_eq_one_iff_mem M₀, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem add_lt_of_lt_sub_left {a b c : Int} (h : b < c - a) : a + b < c

Proof state:
a b c : Int
h✝ : b < c - a
h : a + b < a + (c - a)
⊢ a + b < c

Tactic:
rwa [← Int.add_sub_assoc, Int.add_comm a c, Int.add_sub_cancel] at h

Result:
no goals

Proof state:
a b c : Int
h : b < c - a
⊢ a + b < c

Tactic:
have h := Int.add_lt_add_left h a

Result:
a b c : Int
h✝ : b < c - a
h : a + b < a + (c - a)
⊢ a + b < c
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem Measure.exists_isOpen_measure_lt_top [TopologicalSpace α] (μ : Measure α)
    [IsLocallyFiniteMeasure μ] (x : α) : ∃ s : Set α, x ∈ s ∧ IsOpen s ∧ μ s < ∞

Proof state:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
⊢ ∃ s, x ∈ s ∧ IsOpen s ∧ μ s < ⊤

Tactic:
simpa only [and_assoc] using (μ.finiteAt_nhds x).exists_mem_basis (nhds_basis_opens x)

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem card_union_le (s t : Set α) : Nat.card (↥(s ∪ t)) ≤ Nat.card s + Nat.card t

Proof state:
case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
rw [← @Nat.cast_le Cardinal, Nat.cast_add, Nat.cast_card, Nat.cast_card, Nat.cast_card]

Result:
case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ Cardinal.mk ↑s + Cardinal.mk ↑t

Proof state:
case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ Cardinal.mk ↑s + Cardinal.mk ↑t

Tactic:
exact Cardinal.mk_union_le s t

Result:
no goals

Proof state:
case inl
α : Type u_1
s t : Set α
h : Finite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h

Result:
case inl
α : Type u_1
s t : Set α
h : Finite ↑s ∧ Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Proof state:
case inl
α : Type u_1
s t : Set α
h : Finite ↑s ∧ Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
cases h

Result:
case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Proof state:
case inr
α : Type u_1
s t : Set α
h : Infinite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
exact Nat.card_eq_zero_of_infinite.trans_le (zero_le _)

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
rcases _root_.finite_or_infinite (↥(s ∪ t)) with h | h

Result:
case inl
α : Type u_1
s t : Set α
h : Finite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

case inr
α : Type u_1
s t : Set α
h : Infinite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
-- Mathlib/Data/Vector3.lean
theorem append_left :
    ∀ {m} (i : Fin2 m) (v : Vector3 α m) {n} (w : Vector3 α n), (v +-+ w) (left n i) = v i
  | _, @fz m, v, _, _ => v.consElim fun a _t => by simp [*, left]
  | _, @fs m i, v, n, w => v.consElim fun _a t => by simp [append_left, left]

Proof state:
α : Type u_1
m : ℕ
v : Vector3 α (m + 1)
x✝¹ : ℕ
x✝ : Vector3 α x✝¹
a : α
_t : Vector3 α m
⊢ ((a :: _t) +-+ x✝) (left x✝¹ fz) = (a :: _t) fz

Tactic:
simp [*, left]

Result:
no goals

Proof state:
α : Type u_1
m : ℕ
i : Fin2 m
v : Vector3 α (m + 1)
n : ℕ
w : Vector3 α n
_a : α
t : Vector3 α m
⊢ ((_a :: t) +-+ w) (left n i.fs) = (_a :: t) i.fs

Tactic:
simp [append_left, left]

Result:
no goals
-- Mathlib/Data/Int/WithZero.lean
theorem toNNReal_pos_apply {e : ℝ≥0} (he : e ≠ 0) {x : ℤₘ₀} (hx : x = 0) :
    toNNReal he x = 0

Proof state:
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x = 0
⊢ (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) = 0

Tactic:
split_ifs

Result:
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x = 0
⊢ 0 = 0

Proof state:
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x = 0
⊢ (toNNReal he) x = 0

Tactic:
simp only [toNNReal, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Result:
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x = 0
⊢ (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) = 0

Proof state:
e : ℝ≥0
he : e ≠ 0
x : ℤₘ₀
hx : x = 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals