harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Finsupp/Span.lean
theorem Submodule.exists_finset_of_mem_iSup {ι : Sort _} (p : ι → Submodule R M) {m : M}
    (hm : m ∈ ⨆ i, p i) : ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ i, p i
this : span R {m} ≤ ⨆ i, p i → ∃ s, span R {m} ≤ ⨆ i ∈ s, p i
⊢ ∃ s, m ∈ ⨆ i ∈ s, p i

Tactic:
simp only [Submodule.span_singleton_le_iff_mem] at this

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ i, p i
this : m ∈ ⨆ i, p i → ∃ s, m ∈ ⨆ i ∈ s, p i
⊢ ∃ s, m ∈ ⨆ i ∈ s, p i

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ i, p i
this : m ∈ ⨆ i, p i → ∃ s, m ∈ ⨆ i ∈ s, p i
⊢ ∃ s, m ∈ ⨆ i ∈ s, p i

Tactic:
exact this hm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ i, p i
⊢ ∃ s, m ∈ ⨆ i ∈ s, p i

Tactic:
have :=
  CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (Submodule R M)
    (Submodule.singleton_span_isCompactElement m) p

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ i, p i
this : span R {m} ≤ ⨆ i, p i → ∃ s, span R {m} ≤ ⨆ i ∈ s, p i
⊢ ∃ s, m ∈ ⨆ i ∈ s, p i
-- Mathlib/Data/Real/Basic.lean
theorem ofCauchy_inf (a b) : (⟨⟦a ⊓ b⟧⟩ : ℝ) = ⟨⟦a⟧⟩ ⊓ ⟨⟦b⟧⟩ :=
  show _ = inf _ _ by
    rw [inf_def]
    rfl

Proof state:
a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊓ b⟧ } =
    match { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x1 x2 => x1 ⊓ x2) ⋯ x y }

Tactic:
rfl

Result:
no goals

Proof state:
a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊓ b⟧ } = Real.inf { cauchy := ⟦a⟧ } { cauchy := ⟦b⟧ }

Tactic:
rw [inf_def]

Result:
a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊓ b⟧ } =
    match { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x1 x2 => x1 ⊓ x2) ⋯ x y }
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem IsPurelyInseparable.tower_bot [Algebra E K] [IsScalarTower F E K]
    [IsPurelyInseparable F K] : IsPurelyInseparable F E

Proof state:
case intro
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
x : E
h✝ : (minpoly F ((algebraMap E K) x)).Separable
y : F
h : (algebraMap F K) y = (algebraMap E K) x
⊢ x ∈ (algebraMap F E).range

Tactic:
exact ⟨y, (algebraMap E K).injective (h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm)⟩

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
x : E
h : (minpoly F ((algebraMap E K) x)).Separable
⊢ x ∈ (algebraMap F E).range

Tactic:
obtain ⟨y, h⟩ := inseparable F _ h

Result:
case intro
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
x : E
h✝ : (minpoly F ((algebraMap E K) x)).Separable
y : F
h : (algebraMap F K) y = (algebraMap E K) x
⊢ x ∈ (algebraMap F E).range

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
⊢ IsPurelyInseparable F E

Tactic:
refine ⟨⟨fun x ↦ (isIntegral' F (algebraMap E K x)).tower_bot_of_field⟩, fun x h ↦ ?_⟩

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
x : E
h : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
x : E
h : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Tactic:
rw [IsSeparable, ← minpoly.algebraMap_eq (algebraMap E K).injective] at h

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
x : E
h : (minpoly F ((algebraMap E K) x)).Separable
⊢ x ∈ (algebraMap F E).range
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem exists_fixedPoint' {s : Set α} (hsc : IsComplete s) (hsf : MapsTo f s s)
    (hf : ContractingWith K <| hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
    ∃ y ∈ s, IsFixedPt f y ∧ Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y) ∧
      ∀ n : ℕ, edist (f^[n] x) y ≤ edist x (f x) * (K : ℝ≥0∞) ^ n / (1 - K)

Proof state:
case intro.intro.intro.refine_2
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤
      edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist (f^[n] x) ↑y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

Tactic:
convert hle n

Result:
case h.e'_3
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤
      edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist (f^[n] x) ↑y = edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_eq_length {p : α → Bool} {xs : List α} :
    xs.findIdx p = xs.length ↔ ∀ x ∈ xs, p x = false

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx p xs = xs.length ↔ ∀ (x : α), x ∈ xs → p x = false
⊢ (bif p x then 0 else findIdx p xs + 1) = xs.length + 1 ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = false

Tactic:
simp only [cond_eq_if]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx p xs = xs.length ↔ ∀ (x : α), x ∈ xs → p x = false
⊢ (if p x = true then 0 else findIdx p xs + 1) = xs.length + 1 ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = false

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx p xs = xs.length ↔ ∀ (x : α), x ∈ xs → p x = false
⊢ findIdx p (x :: xs) = (x :: xs).length ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = false

Tactic:
rw [findIdx_cons, length_cons]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx p xs = xs.length ↔ ∀ (x : α), x ∈ xs → p x = false
⊢ (bif p x then 0 else findIdx p xs + 1) = xs.length + 1 ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = false

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ findIdx p [] = [].length ↔ ∀ (x : α), x ∈ [] → p x = false

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx p xs = xs.length ↔ ∀ (x : α), x ∈ xs → p x = false

Tactic:
induction xs with
| nil => simp_all
| cons x xs ih =>
  rw [findIdx_cons, length_cons]
  simp only [cond_eq_if]
  split <;> simp_all [Nat.succ.injEq]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx p xs = xs.length ↔ ∀ (x : α), x ∈ xs → p x = false
⊢ (if p x = true then 0 else findIdx p xs + 1) = xs.length + 1 ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = false

Tactic:
split <;> simp_all [Nat.succ.injEq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem unattach_push {p : α → Prop} {a : { x // p x }} {l : Vector { x // p x } n} :
    (l.push a).unattach = l.unattach.push a.1

Proof state:
α : Type u_1
n : Nat
p : α → Prop
a : { x // p x }
l : Vector { x // p x } n
⊢ (l.push a).unattach = l.unattach.push a.val

Tactic:
simp only [unattach, Vector.map_push]

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem descPochhammer_smeval_eq_ascPochhammer (r : R) (n : ℕ) :
    (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - n + 1)

Proof state:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
ih : (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
⊢ (descPochhammer ℤ (n + 1)).smeval r = (ascPochhammer ℕ (n + 1)).smeval (r - ↑(n + 1) + 1)

Tactic:
rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right, smeval_mul, ih,
  ascPochhammer_succ_left, X_mul, smeval_mul_X, smeval_comp, smeval_sub, ← C_eq_natCast,
  smeval_add, smeval_one, smeval_C]

Result:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
ih : (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
⊢ (ascPochhammer ℕ n).smeval (r - ↑n + 1) * (X.smeval r - ↑n • r ^ 0) =
    (ascPochhammer ℕ n).smeval (X.smeval (r - ↑n) + 1 • (r - ↑n) ^ 0) * (r - ↑n)

Proof state:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
ih : (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
⊢ (ascPochhammer ℕ n).smeval (r - ↑n + 1) * (X.smeval r - ↑n • r ^ 0) =
    (ascPochhammer ℕ n).smeval (X.smeval (r - ↑n) + 1 • (r - ↑n) ^ 0) * (r - ↑n)

Tactic:
simp only [smeval_X, npow_one, npow_zero, zsmul_one, Int.cast_natCast, one_smul]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
⊢ (descPochhammer ℤ 0).smeval r = (ascPochhammer ℕ 0).smeval (r - ↑0 + 1)

Tactic:
simp only [descPochhammer_zero, ascPochhammer_zero, smeval_one, npow_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)

Tactic:
induction n with
| zero => simp only [descPochhammer_zero, ascPochhammer_zero, smeval_one, npow_zero]
| succ n ih =>
  rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right, smeval_mul, ih,
    ascPochhammer_succ_left, X_mul, smeval_mul_X, smeval_comp, smeval_sub, ← C_eq_natCast,
    smeval_add, smeval_one, smeval_C]
  simp only [smeval_X, npow_one, npow_zero, zsmul_one, Int.cast_natCast, one_smul]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem homogeneousComponent_eq_zero'
    (h : ∀ d : σ →₀ ℕ, d ∈ φ.support → d.degree ≠ n) :
    homogeneousComponent n φ = 0

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight fun x => 1) d ≠ n
⊢ (homogeneousComponent n) φ = 0

Tactic:
exact weightedHomogeneousComponent_eq_zero' n φ h

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, d.degree ≠ n
⊢ (homogeneousComponent n) φ = 0

Tactic:
simp_rw [degree_eq_weight_one] at h

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight fun x => 1) d ≠ n
⊢ (homogeneousComponent n) φ = 0
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_gt_sqrtTwoAddSeries (n : ℕ) : 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π

Proof state:
case ha
n : ℕ
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) = √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2)

Tactic:
rw [pow_succ' _ (n + 1), ← mul_assoc, div_mul_cancel₀, mul_comm]

Result:
case h
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ≠ 0

Proof state:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π

Tactic:
refine lt_of_le_of_lt (le_of_eq ?_) this

Result:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) = √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2)

Proof state:
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) < π / 2 ^ (n + 2)

Tactic:
apply sin_lt

Result:
case h
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)

Proof state:
n : ℕ
⊢ 0 < 2 ^ (n + 2)

Tactic:
apply pow_pos

Result:
case ha
n : ℕ
⊢ 0 < 2

Proof state:
n : ℕ
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π

Tactic:
rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ]

Result:
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) < π / 2 ^ (n + 2)

n : ℕ
⊢ 0 < 2 ^ (n + 2)

Proof state:
case h
n : ℕ
⊢ 0 < 2 ^ (n + 2)

n : ℕ
⊢ 0 < 2 ^ (n + 2)

Tactic:
all_goals apply pow_pos; norm_num

Result:
no goals

Proof state:
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) < π / 2 ^ (n + 2)

n : ℕ
⊢ 0 < 2 ^ (n + 2)

Tactic:
focus
  apply sin_lt
  apply div_pos pi_pos

Result:
case h
n : ℕ
⊢ 0 < 2 ^ (n + 2)

n : ℕ
⊢ 0 < 2 ^ (n + 2)

Proof state:
n : ℕ
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π

Tactic:
have : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π := by
  rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ]
  focus
    apply sin_lt
    apply div_pos pi_pos
  all_goals apply pow_pos; norm_num

Result:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π

Proof state:
case h
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)

Tactic:
apply div_pos pi_pos

Result:
case h
n : ℕ
⊢ 0 < 2 ^ (n + 2)

Proof state:
case h
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem inter_ae_eq_empty_of_ae_eq_empty_left (h : s =ᵐ[μ] (∅ : Set α)) :
    (s ∩ t : Set α) =ᵐ[μ] (∅ : Set α)

Proof state:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ ∅ = ∅ ∩ t

Tactic:
rw [empty_inter]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ s ∩ t =ᶠ[ae μ] ∅

Tactic:
convert ae_eq_set_inter h (ae_eq_refl t)

Result:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ ∅ = ∅ ∩ t
-- Mathlib/Algebra/Group/Subgroup/MulOppositeLemmas.lean
theorem op_closure (s : Set G) : (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Subgroup.coe_unop]

Result:
G : Type u_2
inst✝ : Group G
s : Set G
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}

Proof state:
case e_a.h
G : Type u_2
inst✝ : Group G
s : Set G
a : Subgroup Gᵐᵒᵖ
⊢ a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}

Tactic:
exact MulOpposite.unop_surjective.forall

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}

Tactic:
congr with a

Result:
case e_a.h
G : Type u_2
inst✝ : Group G
s : Set G
a : Subgroup Gᵐᵒᵖ
⊢ a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
lemma truncateToReal_le {t : ℝ≥0∞} (t_ne_top : t ≠ ∞) {x : ℝ≥0∞} :
    truncateToReal t x ≤ t.toReal

Proof state:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x : ℝ≥0∞
⊢ (t ⊓ x).toReal ≤ t.toReal

Tactic:
gcongr

Result:
case hb
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x : ℝ≥0∞
⊢ t ≠ ⊤

case h
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x : ℝ≥0∞
⊢ t ⊓ x ≤ t

Proof state:
case hb
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x : ℝ≥0∞
⊢ t ≠ ⊤

case h
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x : ℝ≥0∞
⊢ t ⊓ x ≤ t

Tactic:
exacts [t_ne_top, min_le_left t x]

Result:
no goals

Proof state:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x : ℝ≥0∞
⊢ t.truncateToReal x ≤ t.toReal

Tactic:
rw [truncateToReal]

Result:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
x : ℝ≥0∞
⊢ (t ⊓ x).toReal ≤ t.toReal
-- Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean
theorem Sphere.secondInter_mem {s : Sphere P} {p : P} (v : V) : s.secondInter p v ∈ s ↔ p ∈ s

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 ∈ s ↔ p ∈ s

Tactic:
simp_rw [mem_sphere, Sphere.secondInter_dist]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem preservesMonomorphisms.of_iso {F G : C ⥤ D} [PreservesMonomorphisms F] (α : F ≅ G) :
    PreservesMonomorphisms G :=
  { preserves := fun {X} {Y} f h => by
      suffices G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom from this ▸ mono_comp _ _
      rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.PreservesMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono f
⊢ Mono (G.map f)

Tactic:
suffices G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom from this ▸ mono_comp _ _

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.PreservesMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono f
⊢ G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.PreservesMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono f
⊢ G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom

Tactic:
rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_erase [DecidableEq α] (s : Finset α) {f : α → β} {a : α} (h : f a = 1) :
    ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
h : f a = 1
⊢ ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x

Tactic:
rw [← sdiff_singleton_eq_erase]

Result:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
h : f a = 1
⊢ ∏ x ∈ s \ {a}, f x = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
h : f a = 1
x : α
hx : x ∈ s
hnx : x ∉ s.erase a
⊢ f x = 1

Tactic:
rwa [eq_of_mem_of_not_mem_erase hx hnx]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
h : f a = 1
⊢ ∏ x ∈ s \ {a}, f x = ∏ x ∈ s, f x

Tactic:
refine prod_subset sdiff_subset fun x hx hnx => ?_

Result:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
h : f a = 1
x : α
hx : x ∈ s
hnx : x ∉ s \ {a}
⊢ f x = 1

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
h : f a = 1
x : α
hx : x ∈ s
hnx : x ∉ s \ {a}
⊢ f x = 1

Tactic:
rw [sdiff_singleton_eq_erase] at hnx

Result:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
h : f a = 1
x : α
hx : x ∈ s
hnx : x ∉ s.erase a
⊢ f x = 1
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem adjointAux_adjointAux (A : E →L[𝕜] F) : adjointAux (adjointAux A) = A

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ adjointAux (adjointAux A) = A

Tactic:
ext v

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
v : E
⊢ (adjointAux (adjointAux A)) v = A v

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
v : E
w : F
⊢ ⟪w, (adjointAux (adjointAux A)) v⟫_𝕜 = ⟪w, A v⟫_𝕜

Tactic:
rw [adjointAux_inner_right, adjointAux_inner_left]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
v : E
⊢ (adjointAux (adjointAux A)) v = A v

Tactic:
refine ext_inner_left 𝕜 fun w => ?_

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
v : E
w : F
⊢ ⟪w, (adjointAux (adjointAux A)) v⟫_𝕜 = ⟪w, A v⟫_𝕜
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma map_comp_isoH2_hom :
    map f φ 2 ≫ (isoH2 B).hom = (isoH2 A).hom ≫ H2Map f φ

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ map f φ 2 ≫ (isoH2 B).hom = (isoH2 A).hom ≫ H2Map f φ

Tactic:
simp [← cancel_epi (groupCohomologyπ _ _), H2Map, Category.assoc]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Holder.lean
lemma add (hf : HolderWith C r f) (hg : HolderWith C' r g) :
    HolderWith (C + C') r (f + g) := fun x₁ x₂ => by
  refine le_trans (edist_add_add_le _ _ _ _) <| le_trans (add_le_add (hf x₁ x₂) (hg x₁ x₂)) ?_
  rw [coe_add, add_mul]

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : SeminormedAddCommGroup Y
C C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
x₁ x₂ : X
⊢ ↑C * edist x₁ x₂ ^ ↑r + ↑C' * edist x₁ x₂ ^ ↑r ≤ ↑(C + C') * edist x₁ x₂ ^ ↑r

Tactic:
rw [coe_add, add_mul]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : SeminormedAddCommGroup Y
C C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
x₁ x₂ : X
⊢ edist ((f + g) x₁) ((f + g) x₂) ≤ ↑(C + C') * edist x₁ x₂ ^ ↑r

Tactic:
refine le_trans (edist_add_add_le _ _ _ _) <| le_trans (add_le_add (hf x₁ x₂) (hg x₁ x₂)) ?_

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : SeminormedAddCommGroup Y
C C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
x₁ x₂ : X
⊢ ↑C * edist x₁ x₂ ^ ↑r + ↑C' * edist x₁ x₂ ^ ↑r ≤ ↑(C + C') * edist x₁ x₂ ^ ↑r