harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
theorem contMDiff_one [One M'] : ContMDiff I I' n (1 : M → M')

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
n : WithTop ℕ∞
inst✝ : One M'
⊢ ContMDiff I I' n 1

Tactic:
simp only [Pi.one_def, contMDiff_const]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem supIndep_torsionBy (hq : (S : Set ι).Pairwise <| (IsCoprime on q)) :
    S.SupIndep fun i => torsionBy R M <| q i

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ S.SupIndep fun i => torsionBy R M (q i)

Tactic:
convert supIndep_torsionBySet_ideal (M := M) fun i hi j hj ij =>
    (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij

Result:
case h.e'_6.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝ : ι
⊢ torsionBy R M (q x✝) = torsionBySet R M ↑(Ideal.span {q x✝})

Proof state:
case h.e'_6.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝ : ι
⊢ torsionBy R M (q x✝) = torsionBySet R M ↑(Ideal.span {q x✝})

Tactic:
exact (torsionBySet_span_singleton_eq (R := R) (M := M) _).symm

Result:
no goals
-- Mathlib/Logic/Equiv/Fintype.lean
theorem extendSubtype_apply_of_mem (e : { x // p x } ≃ { x // q x }) (x) (hx : p x) :
    e.extendSubtype x = e ⟨x, hx⟩

Proof state:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ e.extendSubtype x = ↑(e ⟨x, hx⟩)

Tactic:
dsimp only [extendSubtype]

Result:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ (e.subtypeCongr e.toCompl) x = ↑(e ⟨x, hx⟩)

Proof state:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ (sumCompl q) (Sum.map (⇑e) (⇑e.toCompl) ((sumCompl p).symm x)) = ↑(e ⟨x, hx⟩)

Tactic:
rw [sumCompl_apply_symm_of_pos _ _ hx, Sum.map_inl, sumCompl_apply_inl]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ (e.subtypeCongr e.toCompl) x = ↑(e ⟨x, hx⟩)

Tactic:
simp only [subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply]

Result:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ (sumCompl q) (Sum.map (⇑e) (⇑e.toCompl) ((sumCompl p).symm x)) = ↑(e ⟨x, hx⟩)
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tendsto_nat_floor_atTop {α : Type*} [LinearOrderedSemiring α] [FloorSemiring α] :
    Tendsto (fun x : α ↦ ⌊x⌋₊) atTop atTop :=
  Nat.floor_mono.tendsto_atTop_atTop fun x ↦ ⟨max 0 (x + 1), by simp [Nat.le_floor_iff]⟩

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
x : ℕ
⊢ x ≤ ⌊0 ⊔ (↑x + 1)⌋₊

Tactic:
simp [Nat.le_floor_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem ne_of_lt : ∀ {x y : Bool}, x < y → x ≠ y

Proof state:
⊢ ∀ {x y : Bool}, x < y → x ≠ y

Tactic:
decide

Result:
no goals
-- Mathlib/Tactic/ReduceModChar.lean
lemma CharP.isInt_of_mod {e' r : ℤ} {α : Type*} [Ring α] {n n' : ℕ} (inst : CharP α n) {e : α}
    (he : IsInt e e') (hn : IsNat n n') (h₂ : IsInt (e' % n') r) : IsInt e r :=
  ⟨by rw [he.out, CharP.intCast_eq_intCast_mod α n, show n = n' from hn.out, h₂.out, Int.cast_id]⟩

Proof state:
e' r : ℤ
α : Type u_1
inst✝ : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % ↑n') r
⊢ e = ↑r

Tactic:
rw [he.out, CharP.intCast_eq_intCast_mod α n, show n = n' from hn.out, h₂.out, Int.cast_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_filterMap {α} [BEq β] (b : β) (f : α → Option β) (l : List α) :
    count b (filterMap f l) = countP (fun a => f a == some b) l

Proof state:
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
l : List α
⊢ count b (filterMap f l) = countP (fun a => f a == some b) l

Tactic:
rw [count_eq_countP, countP_filterMap]

Result:
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
l : List α
⊢ countP (fun a => (Option.map (fun x => x == b) (f a)).getD false) l = countP (fun a => f a == some b) l

Proof state:
case e_p
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
l : List α
⊢ (fun a => (Option.map (fun x => x == b) (f a)).getD false) = fun a => f a == some b

Tactic:
ext a

Result:
case e_p.h
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
l : List α
a : α
⊢ (Option.map (fun x => x == b) (f a)).getD false = (f a == some b)

Proof state:
case e_p.h.some
β : Type u_1
α : Type u_2
inst✝ : BEq β
b✝ : β
f : α → Option β
l : List α
a : α
b : β
⊢ (Option.map (fun x => x == b✝) (some b)).getD false = (some b == some b✝)

Tactic:
simp

Result:
no goals

Proof state:
case e_p.h
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
l : List α
a : α
⊢ (Option.map (fun x => x == b) (f a)).getD false = (f a == some b)

Tactic:
obtain _ | b := f a

Result:
case e_p.h.none
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
l : List α
a : α
⊢ (Option.map (fun x => x == b) none).getD false = (none == some b)

case e_p.h.some
β : Type u_1
α : Type u_2
inst✝ : BEq β
b✝ : β
f : α → Option β
l : List α
a : α
b : β
⊢ (Option.map (fun x => x == b✝) (some b)).getD false = (some b == some b✝)

Proof state:
case e_p.h.none
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
l : List α
a : α
⊢ (Option.map (fun x => x == b) none).getD false = (none == some b)

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
l : List α
⊢ countP (fun a => (Option.map (fun x => x == b) (f a)).getD false) l = countP (fun a => f a == some b) l

Tactic:
congr

Result:
case e_p
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
l : List α
⊢ (fun a => (Option.map (fun x => x == b) (f a)).getD false) = fun a => f a == some b
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse [CompleteSpace E] {e : E →L[𝕜] F}
    (he : e.IsInvertible) : ContDiffAt 𝕜 n inverse e

Proof state:
case intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
M : E ≃L[𝕜] F
⊢ ContDiffAt 𝕜 n inverse ↑M

Tactic:
exact _root_.contDiffAt_map_inverse M

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E →L[𝕜] F
he : e.IsInvertible
⊢ ContDiffAt 𝕜 n inverse e

Tactic:
rcases he with ⟨M, rfl⟩

Result:
case intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
M : E ≃L[𝕜] F
⊢ ContDiffAt 𝕜 n inverse ↑M
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem eq_zero_of_forall_dual_eq_zero {x : E} (h : ∀ f : Dual 𝕜 E, f x = (0 : 𝕜)) : x = 0 :=
  norm_le_zero_iff.mp (norm_le_dual_bound 𝕜 x le_rfl fun f => by simp [h f])

Proof state:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ∀ (f : Dual 𝕜 E), f x = 0
f : Dual 𝕜 E
⊢ ‖f x‖ ≤ 0 * ‖f‖

Tactic:
simp [h f]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem OrderIso.map_sSup [CompleteLattice β] (f : α ≃o β) (s : Set α) :
    f (sSup s) = ⨆ a ∈ s, f a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ f (sSup s) = ⨆ a ∈ s, f a

Tactic:
simp only [sSup_eq_iSup, OrderIso.map_iSup]

Result:
no goals
-- Mathlib/GroupTheory/Transfer.lean
theorem diff_mul_diff : diff ϕ R S * diff ϕ S T = diff ϕ R T :=
  prod_mul_distrib.symm.trans
    (prod_congr rfl fun q _ =>
      (ϕ.map_mul _ _).symm.trans
        (congr_arg ϕ
          (by simp_rw [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left])))

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
R S T : H.LeftTransversal
inst✝ : H.FiniteIndex
q : G ⧸ H
x✝ : q ∈ univ
⊢ ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ *
      ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩

Tactic:
simp_rw [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIxxMod_antisymm (h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c)
    (h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b) :
    b ≡ a [PMOD p] ∨ c ≡ b [PMOD p] ∨ a ≡ c [PMOD p]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬b ≡ a [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Tactic:
rw [modEq_comm] at h

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
⊢ b ≡ a [PMOD p] ∨ c ≡ b [PMOD p] ∨ a ≡ c [PMOD p]

Tactic:
by_contra! h

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬b ≡ a [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIcoMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIcoMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Tactic:
exact h.2.1 ((toIcoMod_inj _).1 <| h₁₃₂.antisymm h₁₂₃)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Tactic:
rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.2.2] at h₁₂₃

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIcoMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIcoMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Tactic:
rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.1] at h₁₃₂

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIcoMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIcoMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem generator_mem (S : Submodule R M) [S.IsPrincipal] : generator S ∈ S

Proof state:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
this : generator S ∈ span R {generator S}
⊢ generator S ∈ S

Tactic:
convert this

Result:
case h.e'_4
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
this : generator S ∈ span R {generator S}
⊢ S = span R {generator S}

Proof state:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
⊢ generator S ∈ S

Tactic:
have : generator S ∈ span R {generator S} := subset_span (mem_singleton _)

Result:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
this : generator S ∈ span R {generator S}
⊢ generator S ∈ S

Proof state:
case h.e'_4
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
this : generator S ∈ span R {generator S}
⊢ S = span R {generator S}

Tactic:
exact span_singleton_generator S |>.symm

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem orientation_unitsSMul (e : Basis ι R M) (w : ι → Units R) :
    (e.unitsSMul w).orientation = (∏ i, w i)⁻¹ • e.orientation

Proof state:
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det ((↑(∏ i : ι, w i)⁻¹ * ∏ i : ι, ↑(w i)) • (e.unitsSMul w).det)

Tactic:
norm_cast

Result:
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det (↑((∏ i : ι, w i)⁻¹ * ∏ i : ι, w i) • (e.unitsSMul w).det)

Proof state:
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det (↑((∏ i : ι, w i)⁻¹ * ∏ i : ι, w i) • (e.unitsSMul w).det)

Tactic:
simp only [inv_mul_cancel, Units.val_one, one_smul]

Result:
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det (e.unitsSMul w).det

Proof state:
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ (e.unitsSMul w).orientation = (∏ i : ι, w i)⁻¹ • e.orientation

Tactic:
rw [Basis.orientation, Basis.orientation, smul_rayOfNeZero, ray_eq_iff,
  e.det.eq_smul_basis_det (e.unitsSMul w), det_unitsSMul_self, Units.smul_def, smul_smul]

Result:
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det ((↑(∏ i : ι, w i)⁻¹ * ∏ i : ι, ↑(w i)) • (e.unitsSMul w).det)

Proof state:
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det (e.unitsSMul w).det

Tactic:
exact SameRay.rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma zero_rpow {x : ℝ} (hx : x ≠ 0) : rpow (0 : A) x = 0

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
x : ℝ
hx : x ≠ 0
⊢ rpow 0 x = 0

Tactic:
simp [rpow, NNReal.zero_rpow hx]

Result:
no goals
-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem isMittagLeffler_of_surjective (h : ∀ ⦃i j : J⦄ (f : i ⟶ j), (F.map f).Surjective) :
    F.IsMittagLeffler :=
  fun j => ⟨j, 𝟙 j, fun k g => by rw [map_id, types_id, range_id, (h g).range_eq]⟩

Proof state:
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
h : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
j k : J
g : k ⟶ j
⊢ range (F.map (𝟙 j)) ⊆ range (F.map g)

Tactic:
rw [map_id, types_id, range_id, (h g).range_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_filterMap [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.1) :
    Raw.WFImp (m.filterMap f).1

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
⊢ Raw.WFImp (filterMap f m).val

Tactic:
rw [filterMap_eq_filterMapₘ]

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.filterMapₘ f).val

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.filterMapₘ f).val

Tactic:
exact wfImp_filterMapₘ h

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem isLocalization_of_eq_basicOpen {V : X.Opens} (i : V ⟶ U) (e : V = X.basicOpen f) :
    @IsLocalization.Away _ _ f Γ(X, V) _ (X.presheaf.map i.op).hom.toAlgebra

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
V : X.Opens
i : V ⟶ U
e : V = X.basicOpen f
⊢ IsLocalization.Away f ↑Γ(X, V)

Tactic:
subst e

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
i : X.basicOpen f ⟶ U
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
i : X.basicOpen f ⟶ U
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)

Tactic:
convert isLocalization_basicOpen hU f using 3

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
inst✝ : Inhabited elem
c : cont
i : idx
h : ¬dom c i
this : Decidable (dom c i)
⊢ getElem! c i = default

Tactic:
simp [getElem!_def, getElem?_def, h]

Result:
no goals

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
inst✝ : Inhabited elem
c : cont
i : idx
h : ¬dom c i
⊢ getElem! c i = default

Tactic:
have : Decidable (dom c i) := .isFalse h

Result:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
inst✝ : Inhabited elem
c : cont
i : idx
h : ¬dom c i
this : Decidable (dom c i)
⊢ getElem! c i = default
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_gt_three : 3 < π

Proof state:
⊢ 3 < π

Tactic:
pi_lower_bound [23 / 16]

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_const [AddZeroClass G] [Add H] [AddConstMapClass F G H a b] (f : F) :
    f a = f 0 + b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddZeroClass G
inst✝¹ : Add H
inst✝ : AddConstMapClass F G H a b
f : F
⊢ f a = f 0 + b

Tactic:
simpa using map_add_const f 0

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integrableOn_Ioi_norm_cpow_iff {s : ℂ} {t : ℝ} (ht : 0 < t) :
    IntegrableOn (fun x : ℝ ↦ ‖(x : ℂ) ^ s‖) (Ioi t) ↔ s.re < -1

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ‖↑x ^ s‖) (Ioi t) volume
⊢ s.re < -1

Tactic:
refine (integrableOn_Ioi_rpow_iff ht).mp <| h.congr_fun (fun a ha ↦ ?_) measurableSet_Ioi

Result:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ‖↑x ^ s‖) (Ioi t) volume
a : ℝ
ha : a ∈ Ioi t
⊢ ‖↑a ^ s‖ = a ^ s.re

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ‖↑x ^ s‖) (Ioi t) volume
a : ℝ
ha : a ∈ Ioi t
⊢ ‖↑a ^ s‖ = a ^ s.re

Tactic:
rw [Complex.norm_cpow_eq_rpow_re_of_pos (ht.trans ha)]

Result:
no goals

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
⊢ IntegrableOn (fun x => ‖↑x ^ s‖) (Ioi t) volume ↔ s.re < -1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ integrableOn_Ioi_norm_cpow_of_lt h ht⟩

Result:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x => ‖↑x ^ s‖) (Ioi t) volume
⊢ s.re < -1
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem Subgroup.pow_index_mem {G : Type*} [Group G] (H : Subgroup G) [Normal H] (g : G) :
    g ^ index H ∈ H

Proof state:
G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ g ^ H.index ∈ H

Tactic:
rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem im_T_smul : (T • z).im = z.im

Proof state:
z : ℍ
⊢ (T • z).im = z.im

Tactic:
simpa using im_T_zpow_smul z 1

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem coe_ofRepr [DecidableEq ι] (e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) :
    ⇑(OrthonormalBasis.ofRepr e) = fun i => e.symm (EuclideanSpace.single i (1 : 𝕜))

Proof state:
case h
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
x✝ : ι
⊢ EquivLike.coe e.symm (EuclideanSpace.single x✝ 1) = EquivLike.coe e.symm (EuclideanSpace.single x✝ 1)

Tactic:
congr!

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
⊢ ⇑{ repr := e } = fun i => e.symm (EuclideanSpace.single i 1)

Tactic:
dsimp only [DFunLike.coe]

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
⊢ (fun i => EquivLike.coe e.symm (EuclideanSpace.single i 1)) = fun i =>
    EquivLike.coe e.symm (EuclideanSpace.single i 1)

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
⊢ (fun i => EquivLike.coe e.symm (EuclideanSpace.single i 1)) = fun i =>
    EquivLike.coe e.symm (EuclideanSpace.single i 1)

Tactic:
funext

Result:
case h
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
x✝ : ι
⊢ EquivLike.coe e.symm (EuclideanSpace.single x✝ 1) = EquivLike.coe e.symm (EuclideanSpace.single x✝ 1)