harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/PowerBasis.lean
theorem finrank [StrongRankCondition R] (pb : PowerBasis R S) :
    Module.finrank R S = pb.dim

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : StrongRankCondition R
pb : PowerBasis R S
⊢ Module.finrank R S = pb.dim

Tactic:
rw [Module.finrank_eq_card_basis pb.basis, Fintype.card_fin]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem w {A B : Under X} (f : A ⟶ B) : A.hom ≫ f.right = B.hom

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
A B : Under X
f : A ⟶ B
⊢ A.hom ≫ f.right = B.hom

Tactic:
have := f.w

Result:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
A B : Under X
f : A ⟶ B
this : (Functor.fromPUnit X).map f.left ≫ B.hom = A.hom ≫ (𝟭 T).map f.right
⊢ A.hom ≫ f.right = B.hom

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
A B : Under X
f : A ⟶ B
this : (Functor.fromPUnit X).map f.left ≫ B.hom = A.hom ≫ (𝟭 T).map f.right
⊢ A.hom ≫ f.right = B.hom

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[reassoc (attr := simp)]
lemma map_reindex {n₁ n₂ : Type v} (i : n₁ → n₂) {S T : Scheme.{max u v}} (f : S ⟶ T) :
    map n₂ f ≫ reindex i T = reindex i S ≫ map n₁ f

Proof state:
n₁ n₂ : Type v
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ map n₂ f ≫ reindex i T = reindex i S ≫ map n₁ f

Tactic:
apply hom_ext <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Order/UpperLower.lean
theorem IsUpperSet.null_frontier (hs : IsUpperSet s) : volume (frontier s) = 0

Proof state:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ ¬Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)

Tactic:
refine aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_

Result:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
x✝ : ℝ
⊢ x ∈ frontier sᶜ

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
⊢ x ∈
    {x |
        (fun x =>
            Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ

Tactic:
by_cases h : x ∈ closure s <;>
  simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_not_mem,
    indicator_of_mem, Pi.one_apply]

Result:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ ¬Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)

case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ ¬Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)

Proof state:
case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ ¬Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)

Tactic:
exact aux₀ fun _ ↦ hs.exists_subset_ball <| frontier_subset_closure hx

Result:
no goals

Proof state:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
x✝ : ℝ
⊢ x ∈ frontier sᶜ

Tactic:
rwa [frontier_compl]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
⊢ volume (frontier s) = 0

Tactic:
refine measure_mono_null (fun x hx ↦ ?_)
  (Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet _
    (isClosed_closure (s := s)).measurableSet)

Result:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
⊢ x ∈
    {x |
        (fun x =>
            Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
lemma lintegral_le_meas {s : Set α} {f : α → ℝ≥0∞} (hf : ∀ a, f a ≤ 1) (h'f : ∀ a ∈ sᶜ, f a = 0) :
    ∫⁻ a, f a ∂μ ≤ μ s

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∈ s
⊢ f x ≤ s.indicator 1 x

Tactic:
simpa [hx] using hf x

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∉ s
⊢ f x ≤ s.indicator 1 x

Tactic:
simpa [hx] using h'f x hx

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
⊢ f x ≤ s.indicator 1 x

Tactic:
by_cases hx : x ∈ s

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∈ s
⊢ f x ≤ s.indicator 1 x

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∉ s
⊢ f x ≤ s.indicator 1 x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
⊢ ∫⁻ (a : α), f a ∂μ ≤ μ s

Tactic:
apply (lintegral_mono (fun x ↦ ?_)).trans (lintegral_indicator_one_le s)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
⊢ f x ≤ s.indicator 1 x
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma comap_isBase_iff {B : Set α} :
    (N.comap f).IsBase B ↔ N.IsBasis (f '' B) (f '' (f ⁻¹' N.E)) ∧ B.InjOn f ∧ B ⊆ f ⁻¹' N.E

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ N.IsBasis (f '' B) (f '' (N.comap f).E) ∧ InjOn f B ∧ B ⊆ (N.comap f).E ↔
    N.IsBasis (f '' B) (f '' (f ⁻¹' N.E)) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ (N.comap f).IsBase B ↔ N.IsBasis (f '' B) (f '' (f ⁻¹' N.E)) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E

Tactic:
rw [← isBasis_ground_iff, comap_isBasis_iff]

Result:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ N.IsBasis (f '' B) (f '' (N.comap f).E) ∧ InjOn f B ∧ B ⊆ (N.comap f).E ↔
    N.IsBasis (f '' B) (f '' (f ⁻¹' N.E)) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_replicate {k : α} :
    (replicate n (a,b)).lookup k = if n = 0 then none else if k == a then some b else none

Proof state:
case succ
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
α✝ : Type u_1
b : α✝
k : α
n : Nat
ih : lookup k (replicate n (a, b)) = if n = 0 then none else if (k == a) = true then some b else none
⊢ lookup k (replicate (n + 1) (a, b)) = if n + 1 = 0 then none else if (k == a) = true then some b else none

Tactic:
simp only [replicate_succ, lookup_cons]

Result:
case succ
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
α✝ : Type u_1
b : α✝
k : α
n : Nat
ih : lookup k (replicate n (a, b)) = if n = 0 then none else if (k == a) = true then some b else none
⊢ (match k == a with
    | true => some b
    | false => lookup k (replicate n (a, b))) =
    if n + 1 = 0 then none else if (k == a) = true then some b else none

Proof state:
case succ
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
α✝ : Type u_1
b : α✝
k : α
n : Nat
ih : lookup k (replicate n (a, b)) = if n = 0 then none else if (k == a) = true then some b else none
⊢ (match k == a with
    | true => some b
    | false => lookup k (replicate n (a, b))) =
    if n + 1 = 0 then none else if (k == a) = true then some b else none

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
α✝ : Type u_1
b : α✝
k : α
⊢ lookup k (replicate n (a, b)) = if n = 0 then none else if (k == a) = true then some b else none

Tactic:
induction n with
| zero => simp
| succ n ih =>
  simp only [replicate_succ, lookup_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case zero
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
α✝ : Type u_1
b : α✝
k : α
⊢ lookup k (replicate 0 (a, b)) = if 0 = 0 then none else if (k == a) = true then some b else none

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma degree_le_mul_left (p : R[X]) (hq : q ≠ 0) : degree p ≤ degree (p * q)

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
⊢ p.degree ≤ (p * q).degree

Tactic:
obtain rfl | hp := eq_or_ne p 0

Result:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : q ≠ 0
⊢ degree 0 ≤ (0 * q).degree

case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ p.degree ≤ (p * q).degree

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ p.degree ≤ (p * q).degree

Tactic:
rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ ↑p.natDegree ≤ ↑p.natDegree + ↑q.natDegree

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : q ≠ 0
⊢ degree 0 ≤ (0 * q).degree

Tactic:
simp

Result:
no goals

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ ↑p.natDegree ≤ ↑p.natDegree + ↑q.natDegree

Tactic:
exact WithBot.coe_le_coe.2 (Nat.le_add_right _ _)

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem IsWide.eqToHom_mem {S : Subgroupoid C} (Sw : S.IsWide) {c d : C} (h : c = d) :
    eqToHom h ∈ S.arrows c d

Proof state:
case refl
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sw : S.IsWide
c : C
⊢ 𝟙 c ∈ S.arrows c c

Tactic:
apply Sw.id_mem c

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sw : S.IsWide
c d : C
h : c = d
⊢ eqToHom h ∈ S.arrows c d

Tactic:
cases h

Result:
case refl
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sw : S.IsWide
c : C
⊢ eqToHom ⋯ ∈ S.arrows c c

Proof state:
case refl
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sw : S.IsWide
c : C
⊢ eqToHom ⋯ ∈ S.arrows c c

Tactic:
simp only [eqToHom_refl]

Result:
case refl
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sw : S.IsWide
c : C
⊢ 𝟙 c ∈ S.arrows c c
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.pow_dvd_iff_le_multiplicity (hf : FiniteMultiplicity a b) {k : ℕ} :
    a ^ k ∣ b ↔ k ≤ multiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
k : ℕ
⊢ a ^ k ∣ b ↔ k ≤ multiplicity a b

Tactic:
exact_mod_cast hf.emultiplicity_eq_multiplicity ▸ pow_dvd_iff_le_emultiplicity

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem findExistsOneDivLT_min (hi : ¬s ≤[i] 0) {m : ℕ}
    (hm : m < findExistsOneDivLT s i) : ¬ExistsOneDivLT s i m

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
m : ℕ
hm : m < Nat.find ⋯
⊢ ¬MeasureTheory.SignedMeasure.ExistsOneDivLT s i m

Tactic:
exact Nat.find_min _ hm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
m : ℕ
hm : m < MeasureTheory.SignedMeasure.findExistsOneDivLT s i
⊢ ¬MeasureTheory.SignedMeasure.ExistsOneDivLT s i m

Tactic:
classical
rw [findExistsOneDivLT, dif_pos hi] at hm
exact Nat.find_min _ hm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
m : ℕ
hm : m < MeasureTheory.SignedMeasure.findExistsOneDivLT s i
⊢ ¬MeasureTheory.SignedMeasure.ExistsOneDivLT s i m

Tactic:
rw [findExistsOneDivLT, dif_pos hi] at hm

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
m : ℕ
hm : m < Nat.find ⋯
⊢ ¬MeasureTheory.SignedMeasure.ExistsOneDivLT s i m
-- Mathlib/Data/PNat/Prime.lean
theorem eq_one_of_lt_two {n : ℕ+} : n < 2 → n = 1

Proof state:
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1

case a
n : ℕ+
h : n < 2
⊢ 1 ≤ n

Tactic:
swap

Result:
case a
n : ℕ+
h : n < 2
⊢ 1 ≤ n

case a
n : ℕ+
h : n < 2
⊢ n ≤ 1

Proof state:
n : ℕ+
⊢ n < 2 → n = 1

Tactic:
intro h

Result:
n : ℕ+
h : n < 2
⊢ n = 1

Proof state:
case a
n : ℕ+
h : n < 2
⊢ 1 ≤ n

Tactic:
apply PNat.one_le

Result:
no goals

Proof state:
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1

Tactic:
exact PNat.lt_add_one_iff.1 h

Result:
no goals

Proof state:
n : ℕ+
h : n < 2
⊢ n = 1

Tactic:
apply le_antisymm

Result:
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1

case a
n : ℕ+
h : n < 2
⊢ 1 ≤ n
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem modelProd_range_prod_id {H : Type*} {H' : Type*} {α : Type*} (f : H → α) :
    (range fun p : ModelProd H H' ↦ (f p.1, p.2)) = range f ×ˢ (univ : Set H')

Proof state:
H : Type u_5
H' : Type u_6
α : Type u_7
f : H → α
⊢ (range fun p => (f p.1, p.2)) = range f ×ˢ univ

Tactic:
rw [prod_range_univ_eq]

Result:
H : Type u_5
H' : Type u_6
α : Type u_7
f : H → α
⊢ (range fun p => (f p.1, p.2)) = range fun p => (f p.1, p.2)

Proof state:
H : Type u_5
H' : Type u_6
α : Type u_7
f : H → α
⊢ (range fun p => (f p.1, p.2)) = range fun p => (f p.1, p.2)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List α} {k : α} :
    (insertManyIfNewUnit m l).contains k = (m.contains k || l.contains k)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ (insertManyIfNewUnit m l).contains k = (m.contains k || l.contains k)

Tactic:
simp_to_raw using Raw₀.Const.contains_insertManyIfNewUnit_list

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem negSucc_emod (m : Nat) {b : Int} (bpos : 0 < b) : -[m+1] % b = b - 1 - m % b

Proof state:
m : Nat
b : Int
bpos : 0 < b
⊢ -[m+1] % b = b - 1 - ↑m % b

Tactic:
rw [Int.sub_sub, Int.add_comm]

Result:
m : Nat
b : Int
bpos : 0 < b
⊢ -[m+1] % b = b - (↑m % b + 1)

Proof state:
m : Nat
b : Int
bpos : 0 < b
⊢ -[m+1] % b = b - (↑m % b + 1)

Tactic:
match b, eq_succ_of_zero_lt bpos with
| _, ⟨n, rfl⟩ => rfl

Result:
no goals

Proof state:
m : Nat
b : Int
n : Nat
bpos : 0 < ↑n.succ
⊢ -[m+1] % ↑n.succ = ↑n.succ - (↑m % ↑n.succ + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma subset_mul_set {s : Set R} {I : TwoSidedIdeal R} (h : s ⊆ I) (t : Set R):
    s * t ⊆ I

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
x : R
hx : x ∈ s
r : R
⊢ (fun x1 x2 => x1 * x2) x r ∈ ↑I

Tactic:
exact mul_mem_right _ _ _ (h hx)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
⊢ s * t ⊆ ↑I

Tactic:
rintro - ⟨x, hx, r, -, rfl⟩

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
x : R
hx : x ∈ s
r : R
⊢ (fun x1 x2 => x1 * x2) x r ∈ ↑I
-- Mathlib/Data/Sum/Order.lean
theorem noMinOrder_iff [LT α] [LT β] : NoMinOrder (α ⊕ β) ↔ NoMinOrder α ∧ NoMinOrder β :=
  ⟨fun _ =>
    ⟨⟨fun a => by
        obtain ⟨b | b, h⟩ := exists_lt (inl a : α ⊕ β)
        · exact ⟨b, inl_lt_inl_iff.1 h⟩
        · exact (not_inr_lt_inl h).elim⟩,
      ⟨fun a => by
        obtain ⟨b | b, h⟩ := exists_lt (inr a : α ⊕ β)
        · exact (not_inl_lt_inr h).elim
        · exact ⟨b, inr_lt_inr_iff.1 h⟩⟩⟩,
    fun h => @Sum.noMinOrder _ _ _ _ h.1 h.2⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
⊢ ∃ b, b < a

Tactic:
obtain ⟨b | b, h⟩ := exists_lt (inr a : α ⊕ β)

Result:
case intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
b : α
h : inl b < inr a
⊢ ∃ b, b < a

case intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : β
h : inr b < inr a
⊢ ∃ b, b < a

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
b : β
h : inr b < inl a
⊢ ∃ b, b < a

Tactic:
exact (not_inr_lt_inl h).elim

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
⊢ ∃ b, b < a

Tactic:
obtain ⟨b | b, h⟩ := exists_lt (inl a : α ⊕ β)

Result:
case intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : α
h : inl b < inl a
⊢ ∃ b, b < a

case intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
b : β
h : inr b < inl a
⊢ ∃ b, b < a

Proof state:
case intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : α
h : inl b < inl a
⊢ ∃ b, b < a

Tactic:
exact ⟨b, inl_lt_inl_iff.1 h⟩

Result:
no goals

Proof state:
case intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
b : α
h : inl b < inr a
⊢ ∃ b, b < a

Tactic:
exact (not_inl_lt_inr h).elim

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : β
h : inr b < inr a
⊢ ∃ b, b < a

Tactic:
exact ⟨b, inr_lt_inr_iff.1 h⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem repr_scale (x) [NF x] (o) [NF o] : repr (scale x o) = ω ^ repr x * repr o

Proof state:
x : ONote
inst✝¹ : x.NF
o : ONote
inst✝ : o.NF
⊢ (x.scale o).repr = ω ^ x.repr * o.repr

Tactic:
simp only [scale_eq_mul, repr_mul, repr, PNat.one_coe, Nat.cast_one, mul_one, add_zero]

Result:
no goals
-- Mathlib/RepresentationTheory/Basic.lean
theorem ofModule_asAlgebraHom_apply_apply (r : MonoidAlgebra k G)
    (m : RestrictScalars k (MonoidAlgebra k G) M) :
    ((ofModule M).asAlgebraHom r) m =
      (RestrictScalars.addEquiv _ _ _).symm (r • RestrictScalars.addEquiv _ _ _ m)

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ((ofModule M).asAlgebraHom r) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

Tactic:
apply MonoidAlgebra.induction_on r

Result:
case hM
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (g : G),
    ((ofModule M).asAlgebraHom ((of k G) g)) m =
      (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
        ((of k G) g • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

case hadd
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (f g : MonoidAlgebra k G),
    ((ofModule M).asAlgebraHom f) m =
        (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
          (f • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
      ((ofModule M).asAlgebraHom g) m =
          (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
            (g • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
        ((ofModule M).asAlgebraHom (f + g)) m =
          (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
            ((f + g) • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

case hsmul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (r : k) (f : MonoidAlgebra k G),
    ((ofModule M).asAlgebraHom f) m =
        (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
          (f • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
      ((ofModule M).asAlgebraHom (r • f)) m =
        (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
          ((r • f) • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/--
The completed L-function of a Dirichlet character is differentiable, with the following
exceptions: at `s = 1` if `χ` is the trivial character (to any modulus); and at `s = 0` if the
modulus is 1. This result is best possible.

Note both `χ` and `s` are explicit arguments: we will always be able to infer one or other
of them from the hypotheses, but it's not clear which!
-/
lemma differentiableAt_completedLFunction (χ : DirichletCharacter ℂ N) (s : ℂ)
    (hs₀ : s ≠ 0 ∨ N ≠ 1) (hs₁ : s ≠ 1 ∨ χ ≠ 1) :
    DifferentiableAt ℂ (completedLFunction χ) s :=
  ZMod.differentiableAt_completedLFunction _ _ (by have := χ.map_zero'; tauto)
    (by have := χ.sum_eq_zero_of_ne_one; tauto)

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : χ ≠ 1 → ∑ a : ZMod N, χ a = 0
⊢ s ≠ 1 ∨ ∑ j : ZMod N, χ j = 0

Tactic:
tauto

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : N ≠ 1 → χ 0 = 0
⊢ s ≠ 0 ∨ χ 0 = 0

Tactic:
tauto

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
⊢ s ≠ 1 ∨ ∑ j : ZMod N, χ j = 0

Tactic:
have := χ.sum_eq_zero_of_ne_one

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : χ ≠ 1 → ∑ a : ZMod N, χ a = 0
⊢ s ≠ 1 ∨ ∑ j : ZMod N, χ j = 0

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
⊢ s ≠ 0 ∨ χ 0 = 0

Tactic:
have := χ.map_zero'

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : N ≠ 1 → χ 0 = 0
⊢ s ≠ 0 ∨ χ 0 = 0
-- Mathlib/MeasureTheory/PiSystem.lean
theorem has_univ : d.Has univ

Proof state:
α : Type u_3
d : DynkinSystem α
⊢ d.Has univ

Tactic:
simpa using d.has_compl d.has_empty

Result:
no goals
-- Mathlib/Order/Hom/Lattice.lean
theorem cancel_left {g : SupHom β γ} {f₁ f₂ : SupHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => SupHom.ext fun a => hg <| by rw [← SupHom.comp_apply, h, SupHom.comp_apply],
    congr_arg _⟩

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Max α
inst✝¹ : Max β
inst✝ : Max γ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← SupHom.comp_apply, h, SupHom.comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem map_bind [Monad m] [LawfulMonad m] (f : β → γ) (x : m α) (g : α → m β) :
    f <$> (x >>= g) = x >>= fun a => f <$> g a

Proof state:
m : Type u_1 → Type u_2
β γ α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → γ
x : m α
g : α → m β
⊢ (do
      let x ← x
      let a ← g x
      pure (f a)) =
    do
    let a ← x
    f <$> g a

Tactic:
simp [bind_pure_comp]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
β γ α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → γ
x : m α
g : α → m β
⊢ f <$> (x >>= g) = do
    let a ← x
    f <$> g a

Tactic:
rw [← bind_pure_comp, LawfulMonad.bind_assoc]

Result:
m : Type u_1 → Type u_2
β γ α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → γ
x : m α
g : α → m β
⊢ (do
      let x ← x
      let a ← g x
      pure (f a)) =
    do
    let a ← x
    f <$> g a