harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/Over.lean
theorem LiesOver.of_eq_comap [Q.LiesOver p] {F : Type*} [FunLike F B C]
    [AlgHomClass F A B C] (f : F) (h : P = Q.comap f) : P.LiesOver p where
  over

Proof state:
A : Type u_2
inst✝⁷ : CommSemiring A
B : Type u_3
C : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝² : Q.LiesOver p
F : Type u_5
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
h : P = comap f Q
⊢ p = under A P

Tactic:
rw [h]

Result:
A : Type u_2
inst✝⁷ : CommSemiring A
B : Type u_3
C : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝² : Q.LiesOver p
F : Type u_5
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
h : P = comap f Q
⊢ p = under A (comap f Q)

Proof state:
A : Type u_2
inst✝⁷ : CommSemiring A
B : Type u_3
C : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝² : Q.LiesOver p
F : Type u_5
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
h : P = comap f Q
⊢ p = under A (comap f Q)

Tactic:
exact (over_def Q p).trans <|
  congrFun (congrFun (congrArg comap ((f : B →ₐ[A] C).comp_algebraMap.symm)) _) Q

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Equivalence.lean
lemma W_whiskerLeft_iff {P Q : Cᵒᵖ ⥤ A} (f : P ⟶ Q) :
    K.W (whiskerLeft G.op f) ↔ J.W f

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W (whiskerLeft G.op f) ↔ K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W (whiskerLeft G.op f) ↔ J.W f

Tactic:
rw [← W_inverseImage_whiskeringLeft J K G]

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W (whiskerLeft G.op f) ↔ K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/--
Second step in Bojanić's proof of Mahler's theorem (equation (11) of [bojanic74]): show that values
`Δ_[1]^[n + p ^ t] f 0` for large enough `n` are bounded by the max of `(‖f‖ / p ^ s)` and `1 / p`
times a sup over values for smaller `n`.

We use `nnnorm`s on the RHS since `Finset.sup` requires an order with a bottom element.
-/
private lemma bojanic_mahler_step2 {f : C(ℤ_[p], E)} {s t : ℕ}
    (hst : ∀ x y : ℤ_[p], ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s) (n : ℕ) :
    ‖Δ_[1]^[n + p ^ t] f 0‖ ≤ max ↑((Finset.range (p ^ t - 1)).sup
      fun j ↦ ‖Δ_[1]^[n + (j + 1)] f 0‖₊ / p) (‖f‖ / p ^ s)

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖((-1) ^ (n - i) * ↑(n.choose i)) • (f (↑i + ↑(p ^ t)) - f ↑i)‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
calc ‖((-1 : ℤ) ^ (n - i) * n.choose i) • (f (i + ↑(p ^ t)) - f i)‖
_ ≤ ‖f (i + ↑(p ^ t)) - f i‖ := by
  rw [← Int.cast_smul_eq_zsmul ℚ_[p], norm_smul]
  apply mul_le_of_le_one_left (norm_nonneg _)
  simpa only [← coe_intCast] using norm_le_one _
_ ≤ ‖f‖ / p ^ s := by
  apply hst
  rw [Nat.cast_pow, add_sub_cancel_left, norm_pow, norm_p, inv_pow, zpow_neg, zpow_natCast]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem Fintype.linearIndependent_iff [Fintype ι] :
    LinearIndependent R v ↔ ∀ g : ι → R, ∑ i, g i • v i = 0 → ∀ i, g i = 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
H : LinearIndependent R v
g : ι → R
⊢ ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0

Tactic:
simpa using linearIndependent_iff'.1 H Finset.univ g

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i : ι
⊢ ∑ i : ι, g i • v i = 0

Tactic:
rw [← hs]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i : ι
⊢ ∑ i : ι, g i • v i = ∑ i ∈ s, g i • v i

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i✝ i : ι
x✝ : i ∈ Finset.univ
hi : i ∉ s
⊢ g i • v i = 0

Tactic:
rw [hg i hi, zero_smul]

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i : ι
⊢ ∑ i : ι, g i • v i = ∑ i ∈ s, g i • v i

Tactic:
refine (Finset.sum_subset (Finset.subset_univ _) fun i _ hi => ?_).symm

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i✝ i : ι
x✝ : i ∈ Finset.univ
hi : i ∉ s
⊢ g i • v i = 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0

Tactic:
refine
  ⟨fun H g => by simpa using linearIndependent_iff'.1 H Finset.univ g, fun H =>
    linearIndependent_iff''.2 fun s g hg hs i => H _ ?_ _⟩

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i : ι
⊢ ∑ i : ι, g i • v i = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.of_ro_eq_false (u v k : Nat) : ((u ≤ v + k) = False) → v + (k+1) ≤ u

Proof state:
u v k : Nat
⊢ v + k < u → v + (k + 1) ≤ u

Tactic:
omega

Result:
no goals

Proof state:
u v k : Nat
⊢ (u ≤ v + k) = False → v + (k + 1) ≤ u

Tactic:
simp

Result:
u v k : Nat
⊢ v + k < u → v + (k + 1) ≤ u
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem coprime_div_gcd_div_gcd
    (H : 0 < gcd m n) : Coprime (m / gcd m n) (n / gcd m n)

Proof state:
m n : Nat
H : 0 < m.gcd n
⊢ (m / m.gcd n).Coprime (n / m.gcd n)

Tactic:
rw [coprime_iff_gcd_eq_one, gcd_div (gcd_dvd_left m n) (gcd_dvd_right m n), Nat.div_self H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem liftIndepPr1
    (f : (a : α) → motive (Quot.mk r a))
    (h : ∀ (a b : α) (p : r a b), Eq.ndrec (f a) (sound p) = f b)
    (q : Quot r)
    : (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q

Proof state:
case mk
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
f : (a : α) → motive (mk r a)
h : ∀ (a b : α) (p : r a b), Eq.ndrec (f a) ⋯ = f b
a✝ : α
⊢ (lift (Quot.indep f) ⋯ (mk r a✝)).fst = mk r a✝

Tactic:
exact rfl

Result:
no goals

Proof state:
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
f : (a : α) → motive (mk r a)
h : ∀ (a b : α) (p : r a b), Eq.ndrec (f a) ⋯ = f b
q : Quot r
⊢ (lift (Quot.indep f) ⋯ q).fst = q

Tactic:
induction q using Quot.ind

Result:
case mk
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
f : (a : α) → motive (mk r a)
h : ∀ (a b : α) (p : r a b), Eq.ndrec (f a) ⋯ = f b
a✝ : α
⊢ (lift (Quot.indep f) ⋯ (mk r a✝)).fst = mk r a✝
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem le_annihilator_iff {N : Submodule R M} {I : Ideal R} : I ≤ annihilator N ↔ I • N = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ (∀ ⦃x : R⦄, x ∈ I → ∀ n ∈ N, x • n = 0) ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ ⊥

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ I ≤ N.annihilator ↔ I • N = ⊥

Tactic:
simp_rw [← le_bot_iff, smul_le, SetLike.le_def, mem_annihilator]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ (∀ ⦃x : R⦄, x ∈ I → ∀ n ∈ N, x • n = 0) ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ ⊥
-- Mathlib/LinearAlgebra/FreeModule/PID.lean
theorem Ideal.smithCoeffs_ne_zero (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) (i) :
    Ideal.smithCoeffs b I hI i ≠ 0

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ False

Tactic:
apply Basis.ne_zero (Ideal.selfBasis b I hI) i

Result:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ (selfBasis b I hI) i = 0

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ (fun a => ↑a) ((selfBasis b I hI) i) = (fun a => ↑a) 0

Tactic:
simp [hi]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ smithCoeffs b I hI i ≠ 0

Tactic:
intro hi

Result:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ False

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ (selfBasis b I hI) i = 0

Tactic:
refine Subtype.coe_injective ?_

Result:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ (fun a => ↑a) ((selfBasis b I hI) i) = (fun a => ↑a) 0
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_graph {f : L.Functions n} {x : Fin n → M} {y : M} :
    (Formula.graph f).Realize (Fin.cons y x : _ → M) ↔ funMap f x = y

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
f : L.Functions n
x : Fin n → M
y : M
⊢ (graph f).Realize (cons y x) ↔ funMap f x = y

Tactic:
simp only [Formula.graph, Term.realize, realize_equal, Fin.cons_zero, Fin.cons_succ]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
f : L.Functions n
x : Fin n → M
y : M
⊢ (y = funMap f fun i => x i) ↔ funMap f x = y

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
f : L.Functions n
x : Fin n → M
y : M
⊢ (y = funMap f fun i => x i) ↔ funMap f x = y

Tactic:
rw [eq_comm]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem smul_eq_smul [Nontrivial A] (k : 𝕜) (a : A) (ha : (σ a).Nonempty) :
    σ (k • a) = k • σ a

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
⊢ σ (k • a) = k • σ a

Tactic:
rcases eq_or_ne k 0 with (rfl | h)

Result:
case inl
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
ha : (σ a).Nonempty
⊢ σ (0 • a) = 0 • σ a

case inr
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
h : k ≠ 0
⊢ σ (k • a) = k • σ a

Proof state:
case inl
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
ha : (σ a).Nonempty
⊢ σ (0 • a) = 0 • σ a

Tactic:
simpa [ha, zero_smul_set] using (show {(0 : 𝕜)} = (0 : Set 𝕜) from rfl)

Result:
no goals

Proof state:
case inr
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
h : k ≠ 0
⊢ σ (k • a) = k • σ a

Tactic:
exact unit_smul_eq_smul a (Units.mk0 k h)

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_of_not_sigmaFinite (hm : m ≤ m₀) (hμm_not : ¬SigmaFinite (μ.trim hm)) :
    μ[f|m] = 0

Proof state:
case hnc
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm_not : ¬SigmaFinite (μ.trim hm)
⊢ ¬(SigmaFinite (μ.trim hm) ∧ Integrable f μ)

Tactic:
push_neg

Result:
case hnc
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm_not : ¬SigmaFinite (μ.trim hm)
⊢ SigmaFinite (μ.trim hm) → ¬Integrable f μ

Proof state:
case hnc
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm_not : ¬SigmaFinite (μ.trim hm)
⊢ SigmaFinite (μ.trim hm) → ¬Integrable f μ

Tactic:
exact fun h => absurd h hμm_not

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm_not : ¬SigmaFinite (μ.trim hm)
⊢ μ[f|m] = 0

Tactic:
rw [condExp, dif_pos hm, dif_neg]

Result:
case hnc
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm_not : ¬SigmaFinite (μ.trim hm)
⊢ ¬(SigmaFinite (μ.trim hm) ∧ Integrable f μ)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma Y_eq_negY_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0)
    (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W'.negY Q * P z) :
    P y = W'.negY P :=
  mul_left_injective₀ hQz <| by
    linear_combination (norm := ring1) -Y_sub_Y_add_Y_sub_negY hx + hy + hy'

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ (fun a => a * Q z) (P y) = (fun a => a * Q z) (W'.negY P)

Tactic:
linear_combination (norm := ring1) -Y_sub_Y_add_Y_sub_negY hx + hy + hy'

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma fromRows_zero : fromRows (0 : Matrix m₁ n R) (0 : Matrix m₂ n R) = 0

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Semiring R
⊢ fromRows 0 0 = 0

Tactic:
ext (_ | _) _ <;> simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Supported.lean
theorem supportedEquivMvPolynomial_symm_X (s : Set σ) (i : s) :
    (↑((supportedEquivMvPolynomial s).symm (X i : MvPolynomial s R)) : MvPolynomial σ R) = X ↑i :=
  by simp [supportedEquivMvPolynomial]

Proof state:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
i : ↑s
⊢ ↑((supportedEquivMvPolynomial s).symm (X i)) = X ↑i

Tactic:
simp [supportedEquivMvPolynomial]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mem_mapIdx {b : β} {l : List α} :
    b ∈ mapIdx f l ↔ ∃ (i : Nat) (h : i < l.length), f i l[i] = b

Proof state:
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ b ∈ mapIdx f l ↔ ∃ i h, f i l[i] = b

Tactic:
constructor

Result:
case mp
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ b ∈ mapIdx f l → ∃ i h, f i l[i] = b

case mpr
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ (∃ i h, f i l[i] = b) → b ∈ mapIdx f l

Proof state:
case mpr.intro.intro
β : Type u_1
α : Type u_2
f : Nat → α → β
l : List α
i : Nat
h : i < l.length
⊢ ∃ i_1 h_1, (mapIdx f l)[i_1] = f i l[i]

Tactic:
exact ⟨i, by simpa using h, by simp⟩

Result:
no goals

Proof state:
case mpr
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ (∃ i h, f i l[i] = b) → b ∈ mapIdx f l

Tactic:
rintro ⟨i, h, rfl⟩

Result:
case mpr.intro.intro
β : Type u_1
α : Type u_2
f : Nat → α → β
l : List α
i : Nat
h : i < l.length
⊢ f i l[i] ∈ mapIdx f l

Proof state:
case mp
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : List α
h : b ∈ mapIdx f l
⊢ ∃ i h, f i l[i] = b

Tactic:
exact exists_of_mem_mapIdx h

Result:
no goals

Proof state:
case mpr.intro.intro
β : Type u_1
α : Type u_2
f : Nat → α → β
l : List α
i : Nat
h : i < l.length
⊢ f i l[i] ∈ mapIdx f l

Tactic:
rw [mem_iff_getElem]

Result:
case mpr.intro.intro
β : Type u_1
α : Type u_2
f : Nat → α → β
l : List α
i : Nat
h : i < l.length
⊢ ∃ i_1 h_1, (mapIdx f l)[i_1] = f i l[i]

Proof state:
β : Type u_1
α : Type u_2
f : Nat → α → β
l : List α
i : Nat
h : i < l.length
⊢ (mapIdx f l)[i] = f i l[i]

Tactic:
simp

Result:
no goals

Proof state:
case mp
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ b ∈ mapIdx f l → ∃ i h, f i l[i] = b

Tactic:
intro h

Result:
case mp
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : List α
h : b ∈ mapIdx f l
⊢ ∃ i h, f i l[i] = b

Proof state:
β : Type u_1
α : Type u_2
f : Nat → α → β
l : List α
i : Nat
h : i < l.length
⊢ i < (mapIdx f l).length

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem or_cast {x y : BitVec w} (h : w = w') : x.cast h ||| y.cast h = (x ||| y).cast h

Proof state:
case pred
w w' : Nat
x y : BitVec w
h : w = w'
i✝ : Nat
a✝ : i✝ < w'
⊢ (BitVec.cast h x ||| BitVec.cast h y).getLsbD i✝ = (BitVec.cast h (x ||| y)).getLsbD i✝

Tactic:
simp_all [lt_of_getLsbD]

Result:
no goals

Proof state:
w w' : Nat
x y : BitVec w
h : w = w'
⊢ BitVec.cast h x ||| BitVec.cast h y = BitVec.cast h (x ||| y)

Tactic:
ext

Result:
case pred
w w' : Nat
x y : BitVec w
h : w = w'
i✝ : Nat
a✝ : i✝ < w'
⊢ (BitVec.cast h x ||| BitVec.cast h y).getLsbD i✝ = (BitVec.cast h (x ||| y)).getLsbD i✝
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem isSheafFor_top_sieve (P : Cᵒᵖ ⥤ Type w) : IsSheafFor P ((⊤ : Sieve X) : Presieve X)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))

Tactic:
apply isSheafFor_singleton_iso

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (generate (singleton (𝟙 X))).arrows

Tactic:
rw [← isSheafFor_iff_generate]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P ⊤.arrows

Tactic:
rw [← generate_of_singleton_isSplitEpi (𝟙 X)]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (generate (singleton (𝟙 X))).arrows
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem lift_unique (g : S →+* 𝕎 R) (g_compat : ∀ k, (WittVector.truncate k).comp g = f k) :
    lift _ f_compat = g

Proof state:
case a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
i : ℕ
⊢ (lift f f_compat) x - g x ∈ RingHom.ker (truncate i)

Tactic:
simp only [RingHom.mem_ker, g_compat, ← RingHom.comp_apply, truncate_comp_lift, RingHom.map_sub,
  sub_self]

Result:
no goals

Proof state:
case a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
⊢ ∀ (i : ℕ), (lift f f_compat) x - g x ∈ RingHom.ker (truncate i)

Tactic:
intro i

Result:
case a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
i : ℕ
⊢ (lift f f_compat) x - g x ∈ RingHom.ker (truncate i)

Proof state:
case a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
⊢ (lift f f_compat) x = g x

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Result:
case a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
⊢ ∀ (i : ℕ), (lift f f_compat) x - g x ∈ RingHom.ker (truncate i)

Proof state:
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
⊢ lift f f_compat = g

Tactic:
ext1 x

Result:
case a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
⊢ (lift f f_compat) x = g x
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCard_cons (n : ℕ) (a : α) (s) :
    powersetCard (n + 1) (a ::ₘ s) = powersetCard (n + 1) s + map (cons a) (powersetCard n s) :=
  Quotient.inductionOn s fun l => by simp [powersetCard_coe']

Proof state:
α : Type u_1
n : ℕ
a : α
s : Multiset α
l : List α
⊢ powersetCard (n + 1) (a ::ₘ ⟦l⟧) = powersetCard (n + 1) ⟦l⟧ + map (cons a) (powersetCard n ⟦l⟧)

Tactic:
simp [powersetCard_coe']

Result:
no goals